proposition: Lemma mul_xO_r p q : p * q~0 = (p * q)~0.
proof: Proof. induction p; simpl; f_equal; f_equal; trivial. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef