proposition: Lemma mul_sub_distr_r p q r : q<p -> (p-q)*r = p*r-q*r.
proof: Proof. intros H. rewrite 3 (mul_comm _ r). now apply mul_sub_distr_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef