proposition: Lemma rev_tri_ineq : forall a b c : cms_crr Y, AbsSmall (b[-d]c) ((a[-d]b)[-](a[-d]c)).
proof: Proof. intros. unfold AbsSmall in |- *. split. apply shift_leEq_minus. apply shift_plus_leEq'. unfold cg_minus in |- *. cut ([--][--](b[-d]c)[=]b[-d]c). intros. apply leEq_wdr with ((a[-d]b)[+](b[-d]c)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. apply eq_symmetric_unfolded. apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact H. apply cg_inv_inv. astepr (c[-d]b). apply shift_minus_leEq. apply shift_leEq_plus'. apply shift_minus_leEq. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.reals.Intervals