n m d : 0 < m -> NatBezout n m d -> NatBezout m n d. Proof. intros H [a [b p]]. destruct (@equiv_leq_lt_or_eq 0 a _) as [|q]. - exists (n * a.+1 * b.+1 - b), (m * a.+1 * b.+1 - a). rewrite 2 nat_dist_sub_r. apply nat_moveR_nV. rewrite <- nat_add_comm, nat_add_assoc, <- (nat_add_comm d). rewrite <- nat_sub_l_add_r. 2: { apply nat_mul_r_monotone. rewrite 2 nat_mul_succ_r. nrapply (leq_trans _ (leq_add_l _ _)). rapply (leq_trans _ (leq_add_r _ _)). } apply nat_moveL_nV. rewrite nat_add_comm. snrapply (ap011 nat_add p). lhs nrapply nat_mul_comm. rhs_V nrapply nat_mul_assoc. rhs_V nrapply nat_mul_assoc. snrapply ap. lhs_V nrapply nat_mul_assoc. rhs nrapply nat_mul_assoc. apply nat_mul_comm. - destruct q. exists 0, 0. rewrite 2 nat_mul_zero_l, nat_add_zero_r in *. symmetry in p; symmetry. apply equiv_nat_add_zero in p. by destruct p. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes