n m : n <= m -> nat_gcd n (m - n) = nat_gcd n m. Proof. intros H. lhs nrapply nat_gcd_comm. rhs nrapply nat_gcd_comm. rapply nat_gcd_l_sub. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes