n : 0 < n -> n / n = 1. Proof. intros [|m _]; trivial. nrapply (nat_div_unique _ _ _ 0); 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