Qle-pairwise.rst

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Lemma Qle_pairwise :
  ∀ a b c d,
    0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d →
    (a + c)/(b + d) ≤ a/b + c/d.\ccForall{a b c d : \ccQ{}}{0 < a \wedge
                            0 < b \wedge
                            0 < c \wedge 0 < d \Rightarrow{}
                            \ccFrac{ a + c
                            }{ b + d} \le
                            \ccFrac{ a }{ b} +
                            \ccFrac{ c }{ d}}
Proof with Qeauto.\ccForall{a b c d : \ccQ{}}{0 < a \wedge
                            0 < b \wedge
                            0 < c \wedge 0 < d \Rightarrow{}
                            \ccFrac{ a + c
                            }{ b + d} \le
                            \ccFrac{ a }{ b} +
                            \ccFrac{ c }{ d}}
  intros a b c d H.a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
\ccFrac{ a + c }{ b + d} \le
\ccFrac{ a }{ b} + \ccFrac{ c }{ d}
  field_simplify...a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
\ccFrac{ a + c }{ b + d} \le
\ccFrac{ a \times d + c \times b }{ b \times d}
  rewrite <- (Qmult_le_l (b + d)), Qmult_div_r, Qmult_Qdiv_fact...a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
a + c \le
\ccFrac{ (b + d) \times (a \times d + c \times b)
}{ b \times d}
  rewrite <- (Qmult_le_l (b * d)), Qmult_div_r...a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
(b \times d) \times (a + c) \le
(b + d) \times (a \times d + c \times b)
  field_simplify.a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
(b \times d) \times a + (b \times d) \times c \le
\ccPow{ b }{ 2} \times c + (b \times d) \times a +
(b \times d) \times c + 
\ccPow{ d }{ 2} \times a
  rewrite <- (Qminus_le_l (b * d * a)); ring_simplify.a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
(b \times d) \times c \le
\ccPow{ b }{ 2} \times c + (b \times d) \times c +
\ccPow{ d }{ 2} \times a
  rewrite <- (Qminus_le_l (b * d * c)); ring_simplify.a, b, c, d:\ccQ{}
H:0 < a \wedge 0 < b \wedge 0 < c \wedge 0 < d
0 \le
\ccPow{ b }{ 2} \times c +
\ccPow{ d }{ 2} \times a
  Qeauto using Qsqr_0.
Qed.