proposition: Lemma bin_fun_strext_dIR : bin_fun_strext IR IR IR dIR.
proof: Proof. unfold bin_fun_strext in |- *. unfold dIR in |- *. intros. apply cg_minus_strext. apply un_op_strext_unfolded with AbsIR. auto. Qed.
imports: CoRN.metrics.ContFunctions