proposition: Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m).
proof: Proof. intros ????. split; [|rewrite gcd_comm]; now apply gcd_bezout_pos. Qed.
imports: NAxioms NSub NZGcd