proposition: Lemma lt_add_diag_r p q : p < p + q.
proof: Proof. rewrite lt_iff_add. now exists q. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef