n m : 0 < n -> 0 < m -> NatBezout n m (nat_gcd n m) /\ NatBezout m n (nat_gcd n m). Proof. intros H1 H2; split; [| apply nat_bezout_comm]; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes