proposition: Lemma dIR_com : forall x y : IR, dIR_as_CSetoid_fun x y[=]dIR_as_CSetoid_fun y x.
proof: Proof. unfold dIR_as_CSetoid_fun in |- *. unfold dIR in |- *. simpl in |- *. exact AbsIR_minus. Qed.
imports: CoRN.metrics.ContFunctions