nat_dist_l@{} n m k : n * (m + k) = n * m + n * k. Proof. induction n as [|n IHn]; simpl. - reflexivity. - lhs_V nrapply nat_add_assoc. rhs_V nrapply nat_add_assoc. nrapply (ap (nat_add m)). lhs nrapply nat_add_comm. rewrite IHn. lhs_V nrapply nat_add_assoc. nrapply (ap (nat_add (n * m))). nrapply nat_add_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids