proposition: Lemma mul_xI_r p q : p * q~1 = p + (p * q)~0.
proof: Proof. induction p as [p IHp|p IHp| ]; simpl; f_equal; trivial. now rewrite IHp, 2 add_assoc, (add_comm p). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef