proposition: Lemma divide_xO_xO p q : (p~0|q~0) <-> (p|q).
proof: Proof. split; intros (r,H); simpl in *. - rewrite mul_xO_r in H. destr_eq H. now exists r. - exists r; simpl. rewrite mul_xO_r. f_equal; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef