proposition: Lemma sub_sub_distr p q r : r<q -> q-r < p -> p-(q-r) = p+r-q.
proof: Proof. intros. apply add_reg_r with ((q-r)+r). rewrite add_assoc, !sub_add; trivial. rewrite <- (sub_add q r); trivial. now apply add_lt_mono_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef