Require Export SetIsType.

Require Import Arith.
Require Import Omega.


Lemma Match2:
  forall (A B: Prop),
    { A } + { B } ->
    forall (S: Set) (xA xB: S),
      { x: S | (A /\ x = xA) \/ (B /\ x = xB) }
.



Lemma Match2_diff:
  forall (A B: Prop),
    { A } + { B } ->
    (A -> ~B) ->
    (B -> ~A) ->
    forall (S: Set) (xA xB: S),
      { x: S |
        (A -> (x = xA)) /\
        (B -> (x = xB))
      }
.



Lemma Match3:
  forall (A B C: Prop),
    { A } + { B } + { C } ->
    forall (S: Set) (xA xB xC: S),
      { x: S | (A /\ x = xA) \/ (B /\ x = xB) \/ (C /\ x = xC) }
.




Lemma Match3_diff:
  forall (A B C: Prop),
    { A } + { B } + { C } ->
    (A -> ~B /\ ~C) ->
    (B -> ~A /\ ~C) ->
    (C -> ~A /\ ~B) ->
    forall (S: Set) (xA xB xC: S),
      { x: S |
        (A -> (x = xA)) /\
        (B -> (x = xB)) /\
        (C -> (x = xC))
      }
.





Lemma match_comp_nat3_aux_1:
  forall (n m: nat),
    (n < m) -> ~(n = m) /\ ~(n > m).


Lemma match_comp_nat3_aux_2:
  forall (n m: nat),
    (n = m) -> ~(n < m) /\ ~(n > m).


Lemma match_comp_nat3_aux_3:
  forall (n m: nat),
    (n > m) -> ~(n < m) /\ ~(n = m).


Definition match_comp_nat3 (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A): A :=
  match (Match3_diff
    (n < m) (n = m) (n > m) (lt_eq_lt_dec n m)
    (match_comp_nat3_aux_1 n m)
    (match_comp_nat3_aux_2 n m)
    (match_comp_nat3_aux_3 n m)
    A lt_branch eq_branch gt_branch) with
    | (exist x _) => x
  end
.

Lemma match_comp_nat3_lt:
  forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
    (n < m) ->
    (match_comp_nat3 n m A lt_branch eq_branch gt_branch) = lt_branch
.

Lemma match_comp_nat3_eq:
  forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
    (n = m) ->
    (match_comp_nat3 n m A lt_branch eq_branch gt_branch) = eq_branch
.

Lemma match_comp_nat3_gt:
  forall (n m: nat) (A: Set) (lt_branch eq_branch gt_branch: A),
    (n > m) ->
    (match_comp_nat3 n m A lt_branch eq_branch gt_branch) = gt_branch
.


Lemma match_comp_nat2_aux_0:
  forall (n m: nat),
    { n < m } + { n >= m }
.



Lemma match_comp_nat2_aux_1:
  forall (n m: nat),
    (n < m) -> ~(n >= m)
.


Lemma match_comp_nat2_aux_2:
  forall (n m: nat),
    (n >= m) -> ~(n < m)
.


Definition match_comp_nat2 (n m: nat) (A: Set) (lt_branch ge_branch: A): A :=
  match (Match2_diff
    (n < m) (n >= m)
    (match_comp_nat2_aux_0 n m)
    (match_comp_nat2_aux_1 n m)
    (match_comp_nat2_aux_2 n m)
    A lt_branch ge_branch) with
    | (exist x _) => x
  end
.

Lemma match_comp_nat2_lt:
  forall (n m: nat) (A: Set) (lt_branch ge_branch: A),
    (n < m) ->
    (match_comp_nat2 n m A lt_branch ge_branch) = lt_branch
.

Lemma match_comp_nat2_ge:
  forall (n m: nat) (A: Set) (lt_branch ge_branch: A),
    (n >= m) ->
    (match_comp_nat2 n m A lt_branch ge_branch) = ge_branch
.