proposition: Lemma sub_lt p q : p<q -> p-q = 1.
proof: Proof. intros. now apply sub_le, lt_le_incl. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef