proposition: Lemma lt_nle p q : p < q <-> ~ q <= p.
proof: Proof. intros. unfold lt, le. rewrite compare_antisym. destruct compare; split; auto; easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef