nat_div_dist' n m d : (d | m) -> (n + m) / d = n / d + m / d. Proof. intros H. rewrite (nat_add_comm n m). rhs_V nrapply nat_add_comm. rapply nat_div_dist. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes