proposition: Lemma add_sub p q : (p+q)-q = p.
proof: Proof. intros. apply add_reg_r with q. rewrite sub_add; trivial. rewrite add_comm. apply lt_add_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef