``` ```

# Matching Integer Comparisons

``` 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 . ```
Index