n : nat_gcd n 1 = 1. Proof. destruct n; trivial. simpl. destruct n; trivial. rewrite nat_sub_succ_l; only 2: exact _. by rewrite nat_sub_cancel. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes