proposition: Lemma dIR_tri_ineq : tri_ineq dIR_as_CSetoid_fun.
proof: Proof. unfold tri_ineq in |- *. intros x y z. unfold dIR_as_CSetoid_fun in |- *. unfold dIR in |- *. simpl in |- *. astepl (ABSIR (x[+]([--]y[+]y)[-]z)). astepl (ABSIR (x[+][--]y[+](y[-]z))). astepl (ABSIR (x[-]y[+](y[-]z))). apply IR_tri_ineq. apply AbsIR_wd. rational. apply AbsIR_wd. rational. Qed.
imports: CoRN.metrics.ContFunctions