very crap proof that n/2 < n for n > 0

div2.v

Fixpoint nat_lt (a : nat) (b : nat) : bool :=
  match b with
  | 0 => false
  | (S b1) =>
      match a with
      | 0 => true
      | (S a1) => nat_lt a1 b1
      end
  end.

Lemma zero_zero_lt : nat_lt 0 0 = false.
Proof.
  reflexivity.
Qed.

Lemma zero_lt_1 : nat_lt 0 1 = true.
Proof.
  reflexivity.
Qed.

Lemma one_lt_zero : nat_lt 1 0 = false.
Proof.
  reflexivity.
Qed.

Lemma any_lt_zero (n : nat) : nat_lt (S n) 0 = false.
Proof.
  reflexivity.
Qed.

Lemma any_gt_zero (n : nat) : nat_lt 0 (S n) = true.
Proof.
  reflexivity.
Qed.

Lemma m_plus_1_lt_n_plus_1_eq_m_lt_n (m : nat) (n : nat) : nat_lt (S m) (S n) = nat_lt m n.
Proof.
  reflexivity.
Qed.

Fixpoint m_lt_n_eq_m_plus_1_eq_n_plus_1 (m : nat) (n : nat) : nat_lt m n = nat_lt (S m) (S n).
Proof.
  intros.
  case_eq n.
  intros.
  case_eq m.
  intros.
  simpl.
  reflexivity.
  intros.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n (S n0) 0).
  simpl.
  reflexivity.
  intros.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n m (S n0)).
  simpl.
  reflexivity.
Qed.

Lemma any_plus_1_lt_1 (m : nat) : nat_lt (S m) 1 = false.
Proof.
  intros.
  case_eq m.
  reflexivity.
  intros.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n (S n) 0).
  reflexivity.
Qed.

Lemma zero_lt_1_plus_n (n : nat) : nat_lt 0 (S n) = true.
Proof.
  reflexivity.
Qed.

Lemma nat_lt_m_zero_is_false (m : nat) (n : nat) (p : n = 0) : nat_lt m n = false.
Proof.
  case_eq n.
  rewrite p.
  case_eq m.
  intros.
  reflexivity.
  intros.
  reflexivity.
  intros.
  rewrite <- H.
  rewrite p.
  case_eq m.
  reflexivity.
  intros.
  reflexivity.
Qed.

Lemma two_lt_n_means_1_lt_n (n : nat) (p : nat_lt 2 n = true) : nat_lt 1 n = true.
Proof.
  intros.
  case_eq n.
  intros.
  rewrite H in p.
  rewrite (any_lt_zero 1) in p.
  discriminate.
  intros.
  case_eq n0.
  intros.
  rewrite H in p.
  rewrite H0 in p.
  simpl in p.
  discriminate.
  intros.
  simpl.
  reflexivity.
Qed.

Fixpoint sm_lt_n_implies_m_lt_n (m : nat) (n : nat) (p : nat_lt (S m) n = true) : nat_lt m n = true.
Proof.
  intros.
  case_eq m.
  intros.
  case_eq n.
  intros.
  rewrite H0 in p.
  rewrite H in p.
  rewrite one_lt_zero in p.
  discriminate.
  intros.
  case_eq n.
  intros.
  rewrite H1 in H0.
  discriminate.
  intros.
  rewrite (zero_lt_1_plus_n n0).
  reflexivity.
  intros.
  case_eq n.
  intros.
  rewrite H0 in p.
  rewrite (any_lt_zero m) in p.
  discriminate.
  intros.
  rewrite H in p.
  rewrite H0 in p.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n (S n0) n1) in p.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n n0 n1).
  apply (sm_lt_n_implies_m_lt_n n0 n1).
  apply p.
Qed.

Lemma m_less_than_n_implies_m_lt_n_plus_1 (m : nat) (n : nat) (p : nat_lt m n = true) : nat_lt m (S n) = true.
Proof.
  intros.
  case_eq m.
  rewrite (zero_lt_1_plus_n n).
  reflexivity.
  intros.
  rewrite H in p.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n n0 n).
  rewrite (sm_lt_n_implies_m_lt_n n0 n).
  reflexivity.
  apply p.
Qed.

Fixpoint a_b_c_order (a : nat) (b : nat) (c : nat) (p : nat_lt a b = true) (q : nat_lt b c = true) : nat_lt a c = true.
Proof.
  intros.
  case_eq c.
  intros.
  case_eq b.
  intros.
  case_eq a.
  intros.
  rewrite H0 in p.
  rewrite H1 in p.
  simpl in p.
  discriminate.
  intros.
  rewrite H0 in p.
  rewrite H1 in p.
  simpl in p.
  discriminate.
  intros.
  case_eq a.
  intros.
  rewrite H0 in q.
  rewrite H in q.
  simpl in q.
  discriminate.
  intros.
  rewrite H in q.
  rewrite H0 in q.
  simpl in q.
  discriminate.
  intros.
  case_eq b.
  intros.
  case_eq a.
  intros.
  simpl.
  reflexivity.
  intros.
  rewrite H1 in p.
  rewrite H0 in p.
  simpl in p.
  discriminate.
  intros.
  case_eq a.
  intros.
  simpl.
  reflexivity.
  intros.
  rewrite H1 in p.
  rewrite H0 in p.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n n1 n0) in p.
  rewrite H in q.
  rewrite H0 in q.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n n0 n) in q.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n n1 n).
  apply (a_b_c_order n1 n0 n p q).
Qed.

Fixpoint nat_div_2 (x : nat) : nat :=
  match x with
  | 0 => 0
  | S 0 => 0
  | S (S n) => S (nat_div_2 n)
  end.

Lemma div_2_one_minus (n : nat) : nat_div_2 (S (S n)) = S (nat_div_2 n).
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Fixpoint nat_div_2_p_lt_r_with_p_lt_r (n : nat) (r : nat) (p : nat_lt n r = true) : nat_lt (nat_div_2 n) r = true.
Proof.
  intros.
  case_eq n.
  intros.
  case_eq r.
  intros.
  rewrite H in p.
  rewrite H0 in p.
  simpl in p.
  discriminate.
  intros.
  simpl.
  reflexivity.
  intros.
  case_eq r.
  intros.
  rewrite H in p.
  rewrite H0 in p.
  simpl in p.
  discriminate.
  intros.
  case_eq n0.
  intros.
  simpl.
  reflexivity.
  intros.
  rewrite (div_2_one_minus n2).
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n (nat_div_2 n2) n1).
  rewrite H0 in p.
  rewrite H in p.
  rewrite H1 in p.
  rewrite (m_plus_1_lt_n_plus_1_eq_m_lt_n (S n2) n1) in p.
  apply (nat_div_2_p_lt_r_with_p_lt_r n2 n1 (sm_lt_n_implies_m_lt_n n2 n1 p)).
Qed.