Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c: Q+
(a + b) * (c / c) = c * (a / c + b / c)
apply pos_eq;ring_tac.ring_with_nat.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+, (a * b) / a = b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+, (a * b) / a = b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
(a * b) / a = b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
(a * b) / a = a / a * b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
a / a * b = b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
(a * b) / a = a / a * b
apply pos_eq;ring_tac.ring_with_nat.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
a / a * b = b
rewrite pos_recip_r;apply Qpos_mult_1_l.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
/ 1 = 1
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
/ 1 = 1
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
' (/ 1) = ' 1
exact dec_recip_1.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
LeftDistribute mult plus
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
LeftDistribute mult plus
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallabc : Q+, a * (b + c) = a * b + a * c
intros;apply pos_eq,plus_mult_distr_l.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
Meet Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
Meet Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
0 < ' a ⊓ ' b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
~ (' a ⊓ ' b ≤ 0)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ⊓ ' b ≤ 0
Empty
destruct (total_meet_either (' a) (' b)) as [E1|E1];
rewrite E1 in E;(eapply le_iff_not_lt_flip;[exact E|]);
solve_propholds.Defined.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
Join Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
Join Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
0 < ' a ⊔ ' b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
~ (' a ⊔ ' b ≤ 0)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ⊔ ' b ≤ 0
Empty
destruct (total_join_either (' a) (' b)) as [E1|E1];
rewrite E1 in E;(eapply le_iff_not_lt_flip;[exact E|]);
solve_propholds.Defined.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallabcd : Q,
a + b = c + d -> a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallabcd : Q,
a + b = c + d -> a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: a ≤ c
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: a ≤ c
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: a ≤ c
a + b = c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: a ≤ c
d ≤ b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: a + b ≤ c + b
d ≤ b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c + d ≤ c + b
d ≤ b
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c + d ≤ c + b
c + d ≤ c + b
trivial.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
a + b = a + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
b ≤ d
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
a + b ≤ a + d
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
c + d ≤ a + d
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q E: a + b = c + d E1: c ≤ a
c ≤ a
trivial.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallabcd : Q+,
a + b = c + d -> a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallabcd : Q+,
a + b = c + d -> a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q+ E: a + b = c + d
a + b = a ⊔ c + (b ⊓ d)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q+ E: a + b = c + d
' a + ' b = ' c + ' d
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, d: Q+ E: a + b = c + d
' (a + b) = ' c + ' d
rewrite E;reflexivity.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+,
' a ≤ ' b ->
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+,
' a ≤ ' b ->
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
{cb : Q+ &
((a = plus (a / 2) (a / 2)) * (b = plus (a / 2) cb))%type}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
((a = plus (a / 2) (a / 2)) * (b = plus (a / 2) ?Goal))%type
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
0 < ' (a / 2) + (' b - ' a)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
0 ≤ ' b - ' a
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
0 < ' (a / 2)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
0 ≤ ' b - ' a
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
' a ≤ ' b
trivial.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
0 < ' (a / 2)
solve_propholds.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
((a = plus (a / 2) (a / 2)) *
(b =
plus (a / 2)
{|
pos := plus (' (a / 2)) (' b - ' a);
is_pos :=
nonneg_plus_lt_compat_r 0 (' (a / 2))
(' b - ' a)
(snd (flip_nonneg_minus (' a) (' b)) E)
(pos_is_pos (a / 2))
|}))%type
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
a = a / 2 + a / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
b =
a / 2 +
{|
pos := ' (a / 2) + (' b - ' a);
is_pos :=
nonneg_plus_lt_compat_r 0
(' (a / 2)) (' b - ' a)
(snd (flip_nonneg_minus (' a) (' b)) E)
(pos_is_pos (a / 2))
|}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
a = a / 2 + a / 2
apply pos_split2.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
b =
a / 2 +
{|
pos := ' (a / 2) + (' b - ' a);
is_pos :=
nonneg_plus_lt_compat_r 0 (' (a / 2)) (' b - ' a)
(snd (flip_nonneg_minus (' a) (' b)) E)
(pos_is_pos (a / 2))
|}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
' b =
' (a / 2 +
{|
pos := ' (a / 2) + (' b - ' a);
is_pos :=
nonneg_plus_lt_compat_r 0 (' (a / 2))
(' b - ' a)
(snd (flip_nonneg_minus (' a) (' b)) E)
(pos_is_pos (a / 2))
|})
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
' b =
' (a / 2) +
' {|
pos := ' (a / 2) + (' b - ' a);
is_pos :=
nonneg_plus_lt_compat_r 0 (' (a / 2))
(' b - ' a)
(snd (flip_nonneg_minus (' a) (' b)) E)
(pos_mult_compat (' a) (' (/ 2))
(pos_is_pos a)
(pos_dec_recip_compat (' 2)
(Qpos_plus_pr 11)))
|}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
' b = ' (a / 2) + (' (a / 2) + (' b - ' a))
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
' b =
' (a / 2) + (' (a / 2) + (' b - ' (a / 2 + a / 2)))
ring_tac.ring_with_integers (NatPair.Z nat).Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+,
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q+,
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' b ≤ ' a
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' a ≤ ' b
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
apply Qpos_le_lt_min;trivial.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: ' b ≤ ' a
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q+ E: {c : Q+ &
{ca : Q+ &
{cb : Q+ &
((b = plus c ca) * (a = plus c cb))%type}}}
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b, c, cb, ca: Q+ E1: b = c + cb E2: a = c + ca
{c : Q+ &
{ca : Q+ &
{cb : Q+ & ((a = plus c ca) * (b = plus c cb))%type}}}
existsc,ca,cb;auto.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, q < r -> Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, q < r -> Q+
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q E: q < r
0 < r - q
exact (snd (flip_pos_minus _ _) E).Defined.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forall (qr : Q) (E : q < r),
r = q + ' Qpos_diff q r E
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forall (qr : Q) (E : q < r),
r = q + ' Qpos_diff q r E
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q E: q < r
r = q + ' Qpos_diff q r E
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q E: q < r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Haux: forallab : Q,
a ≤ b ->
foralle : Q+,
a < ' e ->
b < ' e ->
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}}
forall (ab : Q) (e : Q+),
a < ' e ->
b < ' e ->
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Haux: forallab : Q,
a ≤ b ->
foralle : Q+,
a < ' e ->
b < ' e ->
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}} a, b: Q e: Q+ E1: a < ' e E2: b < ' e
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Haux: forallab : Q,
a ≤ b ->
foralle : Q+,
a < ' e ->
b < ' e ->
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}} a, b: Q e: Q+ E1: a < ' e E2: b < ' e E: b ≤ a
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Haux: forallab : Q,
a ≤ b ->
foralle : Q+,
a < ' e ->
b < ' e ->
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}} a, b: Q e: Q+ E1: a < ' e E2: b < ' e E: b ≤ a d, d': Q+ E3: b < ' d E4: a < ' d E5: e = d + d'
{d : Q+ &
{d' : Q+ &
((a < ' d) * ((b < ' d) * (e = plus d d')))%type}}
eauto.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
2 / 4 = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
2 / 4 = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Hrw: 4 = 2 * 2
2 / 4 = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Hrw: 4 = 2 * 2
' (2 / 4) = ' (1 / 2)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q Hrw: 4 = 2 * 2
2 / 4 = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
2 / (2 * 2) = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
2 * (/ 2 / 2) = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
(2 / 2) / 2 = 1 / 2
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
1 / 2 = 1 / 2
reflexivity.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q X: IsSemiCRing Q
Unit -> Q
exact (fun_ => 1). (* <- wtf *)Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, abs (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, abs (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (q + r) ⊔ (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
q + r ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (q + r) ≤ abs q + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- q - r ≤ abs q + abs r
apply plus_le_compat;apply Qabs_le_neg_raw.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
q + r ≤ abs q + abs r
apply plus_le_compat;apply Qabs_le_raw.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallxy : Q, abs x - abs y ≤ abs (x - y)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallxy : Q, abs x - abs y ≤ abs (x - y)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q - abs r ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q - abs r + abs r ≤ abs (q - r) + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q ≤ abs (q - r) + abs r
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q ≤ abs (q - r + r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q ≤ abs q
reflexivity.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallxy : Q, abs (abs x - abs y) ≤ abs (x - y)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallxy : Q, abs (abs x - abs y) ≤ abs (x - y)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs (abs q - abs r) ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (abs q - abs r) ⊔ (abs q - abs r) ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (abs q - abs r) ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q - abs r ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
- (abs q - abs r) ≤ abs (q - r)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs r - abs q ≤ abs (r - q)
apply Qabs_triangle_alt_aux.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q q, r: Q
abs q - abs r ≤ abs (q - r)
apply Qabs_triangle_alt_aux.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, q < r -> {s : Q & q < s < r}
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallqr : Q, q < r -> {s : Q & q < s < r}
intros q r E;econstructor;apply Q_average_between,E.Qed.
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q, abs (a - b) = abs (b - a)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q
forallab : Q, abs (a - b) = abs (b - a)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q
abs (a - b) = abs (b - a)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q
abs (- (a - b)) = abs (b - a)
H: Funext H0: Univalence Q: Type Qap: Apart Q Qplus: Plus Q Qmult: Mult Q Qzero: Zero Q Qone: One Q Qneg: Negate Q Qrecip: DecRecip Q Qle: Le Q Qlt: Lt Q QtoField: RationalsToField Q Qrats: Rationals Q Qtrivialapart: TrivialApart Q Qdec: DecidablePaths Q Qmeet: Meet Q Qjoin: Join Q Qlattice: LatticeOrder Qle Qle_total: TotalRelation le Qabs: Abs Q a, b: Q