n : n mod n = 0. Proof. destruct n; trivial. snrapply (nat_mod_unique _ _ 1); only 1: exact _. lhs nrapply nat_add_zero_r. nrapply nat_mul_one_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes