n m k : nat_gcd n (nat_gcd m k) = nat_gcd (nat_gcd n m) k. Proof. nrapply nat_gcd_unique. - intros q H1 H2. rapply nat_divides_r_gcd. - rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)). - apply nat_divides_r_gcd; rapply nat_divides_trans. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes