proposition: Lemma mul_xO_discr p q : p~0 * q <> q.
proof: Proof. induction q; try discriminate. rewrite mul_xO_r; injection; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef