proposition: Lemma zero_fun_strext : forall X : CSetoid, bin_fun_strext X X IR (zero_fun X).
proof: Proof. intro X. unfold bin_fun_strext in |- *. unfold zero_fun in |- *. intros x1 x2 y1 y2 Z. set (H := ap_irreflexive_unfolded IR [0] Z) in *. intuition. Qed.
imports: CoRN.reals.Intervals