n m : (nat_gcd n m | n) /\ (nat_gcd n m | m). Proof. revert n m; snrapply nat_ind_strong; intros n IHn m. destruct n. 1: split; exact _. destruct (IHn (m mod n.+1) _ n.+1) as [H1 H2]. unfold nat_gcd; fold nat_gcd. set (n' := n.+1) in *. split; only 1: exact H2. set (r := m mod n'); rewrite (nat_div_mod_spec m n'); unfold r; clear r. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes