proposition: Lemma divide_xO_xI p q r : (p | q~0) -> (p | r~1) -> (p | q).
proof: Proof. intros (s,Hs) (t,Ht). destruct p. - destruct s as [s|s|]; try easy. simpl in Hs. destr_eq Hs. now exists s. - rewrite mul_xO_r in Ht; discriminate. - exists q; now rewrite mul_1_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef