Require Export Peano_dec.
Require Export Relations.
Require Import CLogic.

Lemma S_O : ∀ n : nat, S n ≠ 0.
Proof.
 intro n.
 red in |- ×.
 intro H.
 generalize O_S.
 intro H0.
 red in H0.
 apply H0 with n.
 apply sym_eq.
 exact H.
Qed.

Definition ap_nat (x y : nat) := ¬ (x = y :>nat).

Infix "{#N}" := ap_nat (no associativity, at level 90).

Lemma ap_nat_irreflexive0 : ∀ x : nat, Not (x{#N}x).
Proof.
 red in |- ×.
 unfold ap_nat in |- ×.
 intros x X.
 apply X.
 auto.
Qed.

Lemma ap_nat_symmetric0 : ∀ x y : nat, (x{#N}y) → y{#N}x.
Proof.
 intros x y.
 unfold ap_nat in |- ×.
 intros X.
 intro Y.
 apply X.
 auto.
Qed.

Lemma ap_nat_cotransitive0 : ∀ x y : nat,
 (x{#N}y) → ∀ z : nat, (x{#N}z) or (z{#N}y).
Proof.
 intros x y X z.
 unfold ap_nat in |- ×.
 case (eq_nat_dec x z).
  intro e.
  right.
  rewrite <- e.
  assumption.
 intro.
 left.
 intro.
 elim n.
 assumption.
Qed.

Lemma ap_nat_tight0 : ∀ x y : nat, Not (x{#N}y) ↔ x = y.
Proof.
 intros x y.
 red in |- ×.
 split.
  unfold ap_nat in |- ×.
  intro H.
  case (eq_nat_dec x y).
   intro e.
   assumption.
  intro n.
  elim H.
  intro H0.
  elim n.
  assumption.
 intro H.
 unfold ap_nat in |- ×.
 intro H0.
 elim H0.
 assumption.
Qed.

Lemma plus_strext0 : ∀ x1 x2 y1 y2 : nat,
 (x1+y1{#N}x2+y2) → (x1{#N}x2) or (y1{#N}y2).
Proof.
 intros x1 x2 y1 y2 H.
 unfold ap_nat in |- ×.
 unfold ap_nat in H.
 case (eq_nat_dec x1 x2).
  intro e.
  right.
  red in |- ×.
  intro H0.
  apply H.
  auto.
 intro n.
 left.
 intro H0.
 elim n.
 assumption.
Qed.

Lemma no_inverse0 : ∀ f : nat → nat, ¬ ((2+f 2) = 0 ∧ (f 2+2) = 0).
Proof.
 intro f.
 simpl in |- ×.
 red in |- ×.
 intro H.
 elim H.
 intros H1 H2.
 set (H3 := O_S (S (f 2))) in ×.
 generalize H3.
 unfold not in |- ×.
 intro H4.
 apply H4.
 omega.
Qed.

Lemma mult_strext0 : ∀ x1 x2 y1 y2 : nat,
 (x1×y1{#N}x2×y2) → (x1{#N}x2) or (y1{#N}y2).
Proof.
 unfold ap_nat in |- ×.
 intros x1 x2 y1 y2 H.
 cut ({x1 = x2} + {x1 ≠ x2}).
  intro H1.
  elim H1.
   intro e.
   right.
   red in |- ×.
   intro H0.
   apply H.
   exact (f_equal2 mult e H0).
  intro X.
  auto.
 apply eq_nat_dec.
Qed.

Lemma not_or:(∀ (p q:nat), (p≠q)-> p<q or q<p):CProp.
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.