proposition: Lemma IR_tri_ineq : forall a b : IR, AbsIR (a[+]b)[<=]AbsIR a[+]AbsIR b.
proof: Proof. intros a b. astepr (AbsIR (AbsIR a[+]AbsIR b)). apply AbsSmall_imp_AbsIR. unfold AbsSmall in |- *. split. apply inv_cancel_leEq. astepr (AbsIR (AbsIR a[+]AbsIR b)). astepl ([--]a[+][--]b). astepr (AbsIR a[+]AbsIR b). apply plus_resp_leEq_both. apply inv_leEq_AbsIR. apply inv_leEq_AbsIR. apply eq_symmetric_unfolded. apply AbsIR_eq_x. astepl (ZeroR[+]ZeroR). apply plus_resp_leEq_both. apply AbsIR_nonneg. apply AbsIR_nonneg. astepr (AbsIR a[+]AbsIR b). apply plus_resp_leEq_both. apply leEq_AbsIR. apply leEq_AbsIR. apply eq_symmetric_unfolded. apply AbsIR_eq_x. astepl (ZeroR[+]ZeroR). apply plus_resp_leEq_both. apply AbsIR_nonneg. apply AbsIR_nonneg. apply AbsIR_eq_x. astepl (ZeroR[+]ZeroR). apply plus_resp_leEq_both. apply AbsIR_nonneg. apply AbsIR_nonneg. Qed.
imports: CoRN.metrics.ContFunctions