lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
intros (x y); apply (nat_elim2 ???? x y);
[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
intros (x y); apply (nat_elim2 ???? x y);
[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;