Commit b8dc0773 authored by Ralf Jung's avatar Ralf Jung

make frac_included into general lemma about < and + of positive fractions

parent 26e93ebf
......@@ -11,14 +11,19 @@ Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
Instance frac_pcore : PCore frac := λ _, None.
Instance frac_op : Op frac := λ x y, (x + y)%Qp.
Lemma frac_included (x y : frac) : x y (x < y)%Qc.
(* TODO: Find better place for this lemma. *)
Lemma Qp_le_sum (x y : Qp) : (x < y)%Qc ( z, y = x + z)%Qp.
Proof.
split.
- intros [z ->%leibniz_equiv]; simpl.
rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
- intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
by rewrite (Qcplus_comm y) Qcplus_assoc Qcplus_opp_r Qcplus_0_l.
- intros [z ->%leibniz_equiv]; simpl.
rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
Qed.
Lemma frac_included (x y : frac) : x y (x < y)%Qc.
Proof. symmetry. exact: Qp_le_sum. Qed.
Corollary frac_included_weak (x y : frac) : x y (x y)%Qc.
Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment