n m d : (d | n) -> (n + m) / d = n / d + m / d. Proof. destruct d. 1: reflexivity. intros [x []]. rewrite nat_div_mul_cancel_r. 2: exact _. rapply nat_div_mul_add_cancel_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes