proposition: Lemma lt_not_add_l p q : ~ p+q < p.
proof: Proof. intro H. elim (lt_irrefl p). apply lt_trans with (p+q); auto using lt_add_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef