proposition: Lemma divide_add_cancel_l p q r : (p | r) -> (p | q + r) -> (p | q).
proof: Proof. intros (s,Hs) (t,Ht). exists (t-s). rewrite mul_sub_distr_r. - rewrite <- Hs, <- Ht. symmetry. apply add_sub. - apply mul_lt_mono_r with p. rewrite <- Hs, <- Ht, add_comm. apply lt_add_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef