Require Import Vbase Relations ClassicalDescription ClassicalChoice.

Set Implicit Arguments.

Inductive fraction :=
  | pe_full
  | pe_half.

Definition fraction_plus x y :=
  match x, y with
    | pe_half, pe_half ⇒ Some pe_full
    | _, _ ⇒ None
  end.

Definition fraction_le x y :=
  x = y ∨ ∃ rem, fraction_plus x rem = Some y.

Lemma fraction_plusC x y : fraction_plus x y = fraction_plus y x.

Lemma fraction_plusA :
  ∀ x y xy (P1: fraction_plus x y = Some xy) z xyz
                (P2: fraction_plus xy z = Some xyz),
    ∃ yz, fraction_plus y z = Some yz ∧ fraction_plus x yz = Some xyz.

Lemma fraction_plus_full_l x : fraction_plus pe_full x = None.

Lemma fraction_plus_full_r x : fraction_plus x pe_full = None.

Lemma fraction_plusK1 x y : fraction_plus x y = Some x → False.

Lemma fraction_plusK2 x y : fraction_plus x y = Some y → False.

Lemma fraction_plusK x y z w :
  fraction_plus x y = Some w →
  fraction_plus x z = Some w →
  y = z.

Lemma fraction_le_refl x :
  fraction_le x x.

Lemma fraction_le_trans x y z :
  fraction_le x y →
  fraction_le y z →
  fraction_le x z.

Lemma fraction_le_antisym x y :
  fraction_le x y →
  fraction_le y x →
  x = y.

Lemma fraction_le1 x y z :
  fraction_plus x y = Some z →
  fraction_le x z.

Lemma fraction_le2 x y z :
  fraction_plus x y = Some z →
  fraction_le y z.

Lemma fraction_le_mon x x' y y' z z' :
  fraction_le x x' →
  fraction_le y y' →
  fraction_plus x y = Some z →
  fraction_plus x' y' = Some z' →
  fraction_le z z'.

Lemma fraction_le_none1 x x' y :
  fraction_plus x y = None →
  fraction_le x x' →
  fraction_plus x' y = None.

Lemma fraction_le_none2 x x' y :
  fraction_plus y x = None →
  fraction_le x x' →
  fraction_plus y x' = None.

Lemma fraction_le_full x :
  fraction_le pe_full x ↔ x = pe_full.

Global Opaque fraction_plus fraction_le.