n m : m <= n -> nat_gcd (n - m) m = nat_gcd n m. Proof. intros H. lhs_V nrapply nat_gcd_l_add_r. by rewrite (nat_add_sub_l_cancel H). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes