fact: Definition Nat_le_neq_lt : ∀ x y : nat, x ≤ y → x ≠ y → (x < y)%nat := λ x y Hxy Hnxy, match le_lt_eq_dec x y Hxy with | left Hle => Hle | right Heq => match Hnxy Heq with end end.
imports: Utf8 QArith NPeano Sorted Psatz