proposition: Lemma dIR_pos_imp_ap : forall x y : IR, [0][<]dIR_as_CSetoid_fun x y -> x[#]y.
proof: Proof. unfold dIR_as_CSetoid_fun in |- *. simpl in |- *. intros x y H. cut (x[#]x or y[#]x). intro H0. apply ap_symmetric_unfolded. elim H0. intro H1. cut False. intuition. cut (Not (x[#]x)). intro H2. exact (H2 H1). apply ap_irreflexive_unfolded. intro H1. exact H1. apply bin_fun_strext_dIR. astepr ZeroR. apply ap_symmetric_unfolded. apply less_imp_ap. exact H. unfold dIR in |- *. astepr (ABSIR ZeroR). apply eq_symmetric_unfolded. apply AbsIRz_isz. apply AbsIR_wd. apply eq_symmetric_unfolded. apply cg_minus_correct. Qed.
imports: CoRN.metrics.ContFunctions