proposition: Theorem mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
proof: Proof. induction p as [p IHp|p IHp| ]; simpl. - rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0). change ((p*q+p*r)~0) with (m+n). rewrite 2 add_assoc; f_equal. rewrite <- 2 add_assoc; f_equal. apply add_comm. - f_equal; auto. - reflexivity. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef