n m : NatBezout n m 1 -> nat_gcd n m = 1. Proof. intros [a [b p]]. rapply nat_gcd_unique. intros q H1 H2. rapply (nat_divides_add_l _ _ (b * m)). destruct p; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes