proposition: Lemma pos_imp_ap_imp_diag_zero : forall (X : CSetoid) (d : CSetoid_bin_fun X X IR), pos_imp_ap d -> nneg d -> diag_zero X d.
proof: Proof. intros X d. unfold pos_imp_ap in |- *. unfold nneg in |- *. intros H H6. unfold diag_zero in |- *. intro x. apply not_ap_imp_eq. red in |- *. intro H0. set (H1 := less_conf_ap IR (d x x) [0]) in *. generalize H1. unfold Iff in |- *. intro H2. elim H2. intros H3 H4. set (H5 := H3 H0) in *. elim H5. generalize H6. intros H7 H8. set (H9 := H7 x x) in *. rewrite -> leEq_def in H9. set (H10 := H9 H8) in *. exact H10. intro H7. set (H8 := H x x) in *. set (H9 := H8 H7) in *. set (H10 := ap_irreflexive_unfolded X x H9) in *. exact H10. Qed.
imports: CoRN.reals.Intervals