proposition: Lemma mul_xI_mul_xO_discr p q r : p~1 * r <> q~0 * r.
proof: Proof. induction r; try discriminate. rewrite 2 mul_xO_r; intro H; destr_eq H; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef