proposition: Lemma not_or:(forall (p q:nat), (p<>q)-> p<q or q<p):CProp.
proof: Proof. simpl. intros p q H. set (H0:=(lt_eq_lt_dec p q)). elim H0. clear H0. intros H0. elim H0. clear H0. intros H0. left. exact H0. clear H0. intros H0. intuition. clear H0. intros H0. right. exact H0. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)