Require Import Vbase Classical QArith.

Set Implicit Arguments.

Global Opaque Qred Qplus.

Lemma Qred_Qred x : Qred (Qred x) = Qred x.

Lemma Qred_zero: Qred 0 = 0.

Lemma Qopp_zero: Qopp 0 = 0.

Lemma Qeq_weaken: ∀ (a b: Q), a = b → a == b.

Lemma Qplus_comm_red: ∀ a b, Qred (a + b) = Qred (b + a).

Lemma Qred_Qred_plus: ∀ a b, Qred (Qred a + b) = Qred (a + b).

Lemma Qred_Qred_plus2: ∀ a b, Qred (a + Qred b) = Qred (a + b).

Lemma Qplus_assoc_red: ∀ a b c, Qred (a + (b + c)) = Qred (a + b + c).

Lemma Qplus_opp_l: ∀ q, Qopp q + q == 0.

Lemma adding_nonnegative_l: ∀ (a b c: Q), a + b ≤ c → a ≥ 0 → b ≤ c.

Lemma adding_nonnegative_r: ∀ (a b c: Q), a + b ≤ c → b ≥ 0 → a ≤ c.

Lemma nonnegative_sum: ∀ (a b: Q), a ≥ 0 → b ≥ 0 → a + b ≥ 0.

Lemma nonnegative_sum_eq_zero: ∀ (a b: Q), a ≥ 0 → b ≥ 0 → a + b == 0 → a == 0 ∧ b == 0.

Lemma Qopp_equal: ∀ (a b: Q), a == b ↔ -a == -b.

Lemma Qneq a b: ¬ a == b → a < b ∨ b < a.


Definition frac (a b: nat) := if (b == 0%nat)%bool then 0 else Z.of_nat a # Pos.of_nat b.

Lemma sum_halves a b: frac a (2 × b) + frac a (2 × b) == frac a b.
  Transparent Qplus.
  Opaque Qplus.

Lemma frac_plus_1: ∀ n, frac (n + 1) 1 == frac n 1 + 1.
  Transparent Qplus.
  Opaque Qplus.

Lemma frac11: frac 1 1 == 1.

Lemma Q_to_frac q : q ≥ 0 → ∃ a b, q == frac a b.