forall a b : nat, a < b -> forall c, a < c |_| c < b. Proof. intros a b E1 c. destruct (le_lt_dec c a) as [E2|E2]. - right. apply nat_le_lt_trans with a;trivial. - left;trivial. Defined.
Require Import