proposition: Lemma diag_zero_imp_pos_imp_ap : forall (X : CSetoid) (d : CSetoid_bin_fun X X IR), diag_zero X d -> pos_imp_ap d.
proof: Proof. intros X d. unfold diag_zero in |- *. unfold pos_imp_ap in |- *. intros H. intros x y H0. cut (x[#]x or x[#]y). intro H1. elim H1. cut (Not (x[#]x)). intros H3 H4. set (H5 := H3 H4) in *. intuition. apply ap_irreflexive_unfolded. intro H2. exact H2. apply (csbf_strext X X IR d). astepl ZeroR. apply less_imp_ap. exact H0. Qed.
imports: CoRN.reals.Intervals