proposition: Lemma Pplus_minus : forall p q, p > q -> q+(p-q) = p.
proof: Proof. intros. rewrite Pos.add_comm. now apply Pos.sub_add, Pos.gt_lt. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef