Load lo_axiom.
Require Import Wf_nat.
(* Proba Caml (ALICE) version 0.09 *)

Section Prog.

Definition Ens_geom (p : R) : Ensemble Flot :=
Ensf (fun x => x <= p)
.

Definition Lt_geom (p : R) : Flot -> Flot -> Prop :=
Lt_ensf (fun x => x <= p)
.

Theorem Wf_lt_geom : forall (p:R), well_founded (Lt_geom p).
intros.
unfold Lt_geom.
apply Wf_lt_ensf with p (p + 1).
apply Rle_refl.
apply Rlt_not_le.
apply Rlt_plus_1.
Qed.

Theorem Wf_lt_geom_ind : forall (p : R) (P:Flot -> Prop),
(forall x:Flot, (forall y:Flot, Lt_geom p y x -> P y) -> P x) ->
forall a:Flot, P a.
intro.
apply well_founded_ind.
apply Wf_lt_geom.
Qed.

Variable bernoulli : (R ->> (o bool)).

Hypothesis Hyp_bernoulli :
Double_triangle bernoulli (fun _ => True) (fun p f =>
0 <= p -> p <= 1 ->
Double_carre f (fun _ => True) (fun s y _ => Proba_locale s (y = true) = p)
).

Hypothesis Hyp_bernoulli_conso :
Triangle bernoulli (fun p f =>
0 <= p -> p <= 1 ->
Carre f (fun s y t => exists x, s = x::t /\ (y = true -> x <= p) /\ (y = false -> ~(x <= p)))
).

Variable geometric : (R ->> (o nat)).

Hypothesis Hyp_geometric : 
((Terminaison_triangle geometric (fun p_0 => ((forall f_1, (Terminaison_triangle f_1 (fun a_16 => ((f_1 = bernoulli) /\ (a_16 = p_0))))) /\ (forall f_2, (Terminaison_triangle f_2 (fun a_17 => ((forall f_1, (Terminaison_triangle f_1 (fun a_16 => ((f_1 = bernoulli) /\ (a_16 = p_0))))) /\ (((Terminaison_triangle f_2 (fun berp_0 => True)) /\ (f_2 |> fun berp_0 y_22 => ((Terminaison_carre y_22 (fun s_0 => ((Terminaison_carre y_22 (fun s'_0 => (((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Lt_geom p) berp_0 p_0 bernoulli s'_0 s_0) /\ ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Ens_geom p) berp_0 p_0 bernoulli s'_0)))) /\ ((forall m_0, ((m_0 = berp_0) -> ((exists b_15, (exists s_1, {s_0 >> m_0 ~> b_15 >> s_1})) /\ (forall b_15, (forall s_1, ({s_0 >> m_0 ~> b_15 >> s_1} -> ((forall b_16 : bool, True) /\ (forall m_2, ((forall b_16 : bool, True) -> ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> ((Terminaison_carre m_2 (fun s_2 => True)) /\ (m_2 [] fun s_2 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_2))))) /\ ((b_16 = false) -> ((Terminaison_carre m_2 (fun s_3 => (forall m_1, ((m_1 = y_22) -> ((exists x_5, (exists s_4, {s_3 >> m_1 ~> x_5 >> s_4})) /\ (forall x_5, (forall s_4, ({s_3 >> m_1 ~> x_5 >> s_4} -> (forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5))))))))))))) /\ (m_2 [] fun s_3 y_20 t_1 => (exists m_1, ((m_1 = y_22) /\ (exists x_5, (exists s_4, ({s_3 >> m_1 ~> x_5 >> s_4} /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> y_20)))) /\ (t_1 = s_4))))))))))))) -> ((exists x_6, (exists s_5, {s_1 >> m_2 ~> x_6 >> s_5})) /\ (forall x_6 : bool, (forall s_5 : bool, True))))))))))))) /\ ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Ens_geom p) berp_0 p_0 bernoulli s_0))))) /\ (y_22 [] fun s_0 y_21 t_2 => (exists m_0, ((m_0 = berp_0) /\ (exists b_15, (exists s_1, ({s_0 >> m_0 ~> b_15 >> s_1} /\ (exists m_2, ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> ((Terminaison_carre m_2 (fun s_2 => True)) /\ (m_2 [] fun s_2 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_2))))) /\ ((b_16 = false) -> ((Terminaison_carre m_2 (fun s_3 => (forall m_1, ((m_1 = y_22) -> ((exists x_5, (exists s_4, {s_3 >> m_1 ~> x_5 >> s_4})) /\ (forall x_5, (forall s_4, ({s_3 >> m_1 ~> x_5 >> s_4} -> (forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5))))))))))))) /\ (m_2 [] fun s_3 y_20 t_1 => (exists m_1, ((m_1 = y_22) /\ (exists x_5, (exists s_4, ({s_3 >> m_1 ~> x_5 >> s_4} /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> y_20)))) /\ (t_1 = s_4))))))))))))) /\ (exists x_6, (exists s_5, ({s_1 >> m_2 ~> x_6 >> s_5} /\ ((y_21 = x_6) /\ (t_2 = s_5)))))))))))))))) /\ (exists f_1, (exists a_16, (((f_1 = bernoulli) /\ (a_16 = p_0)) /\ (a_16 -- f_1 --> a_17)))))))))))) /\ (geometric |> fun p_0 y_23 => (exists f_2, (exists a_17, ((((Terminaison_triangle f_2 (fun berp_0 => True)) /\ (f_2 |> fun berp_0 y_22 => ((Terminaison_carre y_22 (fun s_0 => ((Terminaison_carre y_22 (fun s'_0 => (((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Lt_geom p) berp_0 p_0 bernoulli s'_0 s_0) /\ ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Ens_geom p) berp_0 p_0 bernoulli s'_0)))) /\ ((forall m_0, ((m_0 = berp_0) -> ((exists b_15, (exists s_1, {s_0 >> m_0 ~> b_15 >> s_1})) /\ (forall b_15, (forall s_1, ({s_0 >> m_0 ~> b_15 >> s_1} -> ((forall b_16 : bool, True) /\ (forall m_2, ((forall b_16 : bool, True) -> ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> ((Terminaison_carre m_2 (fun s_2 => True)) /\ (m_2 [] fun s_2 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_2))))) /\ ((b_16 = false) -> ((Terminaison_carre m_2 (fun s_3 => (forall m_1, ((m_1 = y_22) -> ((exists x_5, (exists s_4, {s_3 >> m_1 ~> x_5 >> s_4})) /\ (forall x_5, (forall s_4, ({s_3 >> m_1 ~> x_5 >> s_4} -> (forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5))))))))))))) /\ (m_2 [] fun s_3 y_20 t_1 => (exists m_1, ((m_1 = y_22) /\ (exists x_5, (exists s_4, ({s_3 >> m_1 ~> x_5 >> s_4} /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> y_20)))) /\ (t_1 = s_4))))))))))))) -> ((exists x_6, (exists s_5, {s_1 >> m_2 ~> x_6 >> s_5})) /\ (forall x_6 : bool, (forall s_5 : bool, True))))))))))))) /\ ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Ens_geom p) berp_0 p_0 bernoulli s_0))))) /\ (y_22 [] fun s_0 y_21 t_2 => (exists m_0, ((m_0 = berp_0) /\ (exists b_15, (exists s_1, ({s_0 >> m_0 ~> b_15 >> s_1} /\ (exists m_2, ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> ((Terminaison_carre m_2 (fun s_2 => True)) /\ (m_2 [] fun s_2 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_2))))) /\ ((b_16 = false) -> ((Terminaison_carre m_2 (fun s_3 => (forall m_1, ((m_1 = y_22) -> ((exists x_5, (exists s_4, {s_3 >> m_1 ~> x_5 >> s_4})) /\ (forall x_5, (forall s_4, ({s_3 >> m_1 ~> x_5 >> s_4} -> (forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5))))))))))))) /\ (m_2 [] fun s_3 y_20 t_1 => (exists m_1, ((m_1 = y_22) /\ (exists x_5, (exists s_4, ({s_3 >> m_1 ~> x_5 >> s_4} /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_1 => True)) /\ (f_0 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> y_20)))) /\ (t_1 = s_4))))))))))))) /\ (exists x_6, (exists s_5, ({s_1 >> m_2 ~> x_6 >> s_5} /\ ((y_21 = x_6) /\ (t_2 = s_5)))))))))))))))) /\ (exists f_1, (exists a_16, (((f_1 = bernoulli) /\ (a_16 = p_0)) /\ (a_16 -- f_1 --> a_17))))) /\ (a_17 -- f_2 --> y_23))))))
.

Theorem Concl_geometric_termine :
Double_triangle geometric (fun _ => True) (fun p y =>
0 <= p ->
p <= 1 ->
Terminaison_carre y (Ens_geom p)
)
.
generalize Hyp_geometric Hyp_bernoulli Hyp_bernoulli_conso.
clear Hyp_geometric  Hyp_bernoulli Hyp_bernoulli_conso.
unfold Double_triangle.
unfold Double_carre.
unfold Terminaison_triangle.
unfold Terminaison_carre.
unfold Triangle.
unfold Carre.
intuition.
apply H.
intuition.
subst.
apply H1.
trivial.
generalize (H0 _ _ H3).
intros.
casser_les_cailloux.
subst.
generalize (H13 _ _ H9).
intros.
casser_les_cailloux.
generalize H6.
apply (Wf_lt_geom_ind a
(fun s0 =>  Ens_geom a s0 -> exists y : nat, (exists t : Flot, {s0 >> b ~> y >> t})

)
).
intros.
apply H10.
intuition.
subst.
generalize (H2 a x0).
intuition.
subst.
casser_les_cailloux.
subst.
generalize H16 H15 H20.
clear H16 H15 H20.
case b_15.
intuition. (* le cas true se règle directement. *)
intuition.
apply H18.
intros.
subst.
intuition.
generalize (Hyp_bernoulli_conso _ _ H11 H4 H5).
intros.
generalize (H17 _ _ _ H16).
intuition.
casser_les_cailloux.
intuition.
assert (In _ (Ens_geom a) s_1).
unfold Ens_geom.
apply Ensf_sous_flot with x2.
rewrite <- H21.
trivial.
trivial.
apply H7.
2 : trivial.
rewrite H21.
unfold Lt_geom.
apply Lt_ensf_sous_flot_1.
trivial.
trivial.
Qed.

Fixpoint Ens_geom_n (p : R) (n:nat) {struct n} : Ensemble Flot :=
match n with
| Zero => Produit_ensembles_flots (fun x => x <= p) (Full_set _)
| Succ n' => Produit_ensembles_flots (fun x => ~(x <= p)) (Ens_geom_n p n')
end.

Lemma Ens_geom_n_ens : forall (p:R) (n:nat),
Included _ (Ens_geom_n p n) (Ens_geom p).
intro p.
induction n.
compute.
intro x.
case x.
intros.
inversion H.
apply ensf_0.
trivial.
unfold Ens_geom_n.
fold Ens_geom_n.
unfold Included.
unfold Included in IHn.
intro x.
case x.
intros.
unfold Produit_ensembles_flots in H.
unfold In in H.
inversion H.
unfold Ens_geom.
apply ensf_S.
trivial.
apply IHn.
trivial.
Qed.

Theorem Concl_geometric_ensemble :
Triangle geometric (fun p g =>
0 <= p -> p <= 1 ->
forall n : nat,
((fun s => exists y, exists t, {s >> g ~> y >> t} /\ y = n) : Ensemble Flot) =
Ens_geom_n p n
)
.
generalize Hyp_geometric Hyp_bernoulli Hyp_bernoulli_conso.
clear Hyp_geometric  Hyp_bernoulli Hyp_bernoulli_conso.
unfold Double_triangle.
unfold Double_carre.
unfold Terminaison_triangle.
unfold Terminaison_carre.
unfold Triangle.
unfold Carre.
intuition.
casser_les_cailloux.
generalize (Concl_geometric_termine).
unfold Double_triangle.
unfold Triangle.
unfold Terminaison_carre.
intuition.
generalize (H8 _ _ H3 H4 H5).
clear H8.
intros.
casser_les_cailloux.
subst.
generalize (H0 _ _ H3).
clear H0.
intros.
casser_les_cailloux.
subst.
generalize (H13 _ _ H9).
clear H13.
intros.
casser_les_cailloux.
subst.
generalize (Hyp_bernoulli_conso _ _ H11 H4 H5).
clear Hyp_bernoulli_conso.
intros.

induction n.

apply Extensionality_Ensembles.
split.
compute.
intro.
case x1.
intros.
casser_les_cailloux.
subst.
split.
2 : apply Full_intro.
generalize (H12 _ _ _ H14).
intros.
casser_les_cailloux.
subst.
generalize (H0 _ _ _ H15).
intros.
casser_les_cailloux.
injection H13.
intros.
subst.
generalize H21 H17 H20 H16.
clear H13 H21 H17 H20 H16.
case x4.
intuition.
intuition.
generalize (H21 _ _ _ H19).
intros.
casser_les_cailloux.
subst.
generalize (H28 _ _ H26).
intros.
discriminate.
unfold Included.
intros.
compute.
generalize (Ens_geom_n_ens a 0).
intros.
unfold Included in H14.
generalize (H14 _ H13).
intros.
generalize (H6 _ H15).
intros.
casser_les_cailloux.
exists x2.
exists x3.
split.
trivial.
generalize (H12 _ _ _ H16).
intros.
casser_les_cailloux.
subst.
generalize (H0 _ _ _ H18).
intros.
casser_les_cailloux.
subst.
compute in H13.
inversion_clear H13.
clear H21.
generalize H24 H20 H23 H19.
clear  H24 H20 H23 H19.
case x5.
intros.
generalize (refl_equal true).
intros.
generalize (H19 H13).
intros.
casser_les_cailloux.
generalize (H26 _ _ _ H22).
intuition.
intros.
generalize (refl_equal false).
intros.
case (H24 H13 H17).

apply Extensionality_Ensembles.
split.
unfold Included.
unfold In.
intros.
casser_les_cailloux.
subst.
generalize (H12 _ _ _ H14).
intros.
casser_les_cailloux.
subst.
generalize (H0 _ _ _ H15).
intros.
casser_les_cailloux.
subst. 
generalize H21 H17 H20 H16.
clear H21 H17 H20 H16.
case x4.
intuition.
generalize (H18 _ _ _ H19).
intuition.
discriminate.
intuition.
unfold Ens_geom_n.
fold Ens_geom_n.
unfold Produit_ensembles_flots.
unfold In.
split.
trivial.
rewrite <- IHn.
generalize (H21 _ _ _ H19).
intros.
casser_les_cailloux.
subst.
exists x3.
exists x7.
split.
trivial.
generalize (H28 _ _ H26).
intros.
injection H18.
intros.
rewrite H23.
trivial.

unfold Included.
intros.
generalize H13.
unfold Ens_geom_n.
fold Ens_geom_n.
unfold Produit_ensembles_flots.
unfold In.
generalize H13.
clear H13.
case x1.
intros.
inversion_clear H14.
generalize (Ens_geom_n_ens a (S n)).
unfold Included.
intros.
generalize (H14 _ H13).
intros.
generalize (H6 _ H17).
intros.
casser_les_cailloux.
exists x2.
exists x3.
split.
trivial.
generalize (H12 _ _ _ H18).
intros.
casser_les_cailloux.
subst.
generalize (H0 _ _ _ H20).
intros.
casser_les_cailloux.
injection H19.
intros.
subst.
clear H19.
generalize H26 H22 H25 H21.
clear H26 H22 H25 H21.
case x5.
intuition.
intuition.
generalize (H26 _ _ _ H24).
intros.
casser_les_cailloux.
subst.
generalize (H33 _ _ H31).
intros.
rewrite H23.
generalize H16.
rewrite <- IHn.
intros.
casser_les_cailloux.
subst.
generalize (Fonctionnalite_carre _ _ _ _ _ _ _ H30 H27).
intuition.

Qed.

Theorem Ens_geom_n_rectangle :
forall p : R,
0 <= p -> p <= 1 ->
forall n : nat,
Est_rectangle Espace_elem_flot (Ens_geom_n p n)
.
casser_les_cailloux.
induction n.
unfold Ens_geom_n.
apply est_rectangle_n.
compute.
intros.
casser_les_cailloux.
apply H5.
exists 0.
exists p.
assert (Intersection R (fun x : R => (0 < x \/ 0 = x) /\ (x < 1 \/ x = 1))
  (fun x : R => x < p \/ x = p) =
(fun x : R => (0 < x \/ 0 = x) /\ (x < p \/ x = p))

).
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H7.
compute in H9.
inversion H9.
split.
trivial.
trivial.
compute.
intros.
inversion_clear H7.
apply Intersection_intro.
compute.
split.
trivial.
apply Rle_trans with p.
trivial.
trivial.
trivial.
trivial.
rewrite Full_set_is_true.
apply est_rectangle_0.

unfold Ens_geom_n.
fold Ens_geom_n.
apply est_rectangle_n.
2 : trivial.
compute.
intros.
casser_les_cailloux.
apply (H3 (fun x => x <= p)).
apply H5.
exists 0.
exists p.
assert (Intersection R (fun x : R => (0 < x \/ 0 = x) /\ (x < 1 \/ x = 1))
  (fun x : R => x < p \/ x = p) =
(fun x : R => (0 < x \/ 0 = x) /\ (x < p \/ x = p))

).
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H7.
compute in H9.
inversion H9.
split.
trivial.
trivial.
compute.
intros.
inversion_clear H7.
apply Intersection_intro.
compute.
split.
trivial.
apply Rle_trans with p.
trivial.
trivial.
trivial.
trivial.
Qed.

Theorem Ens_geom_n_mesurable : 
forall p : R,
0 <= p -> p <= 1 ->
forall n : nat,
In _ Espace_flots (Ens_geom_n p n)
.
casser_les_cailloux.
intros.
compute.
intros.
casser_les_cailloux.
apply H5.
generalize (Ens_geom_n_rectangle _ H1 H2 n).
compute.
trivial.
Qed.

Lemma tech1 : forall p : R,
0 <= p -> p <= 1 ->
In _ Espace_elem_flot (fun x => x <= p).
intros.
unfold Espace_elem_flot.
unfold B01.
unfold Boreliens.
rewrite <- (sigma_est_sigma2).
apply sigma_0.
compute.
exists 0.
exists p.
assert (
Intersection R (fun x : R => (0 < x \/ 0 = x) /\ (x < 1 \/ x = 1))
    (fun x : R => x < p \/ x = p) =
  (fun x : R => (0 < x \/ 0 = x) /\ (x < p \/ x = p))
).
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H1.
inversion_clear H2.
compute in H3.
intuition.
compute.
intros.
apply Intersection_intro.
compute.
split.
intuition.
apply Rle_trans with p.
intuition.
trivial.
intuition.
trivial.
Qed.

Lemma tech2 :
forall p : R,
0 <= p -> p <= 1 ->
Eef_mesure (fun x => x <= p) = p.
intros.
unfold Eef_mesure.
rewrite B01_etendu.
assert (
Intersection R (fun x : Element_flot => x <= p) U01 =
Intervalle_ferme 0 p
).
apply Extensionality_Ensembles.
split.
compute.
intros.
inversion_clear H1.
inversion_clear H3.
compute in H2.
intuition.
compute.
intros.
inversion_clear H1.
apply Intersection_intro.
compute.
trivial.
compute.
split.
trivial.
apply Rle_trans with p.
trivial.
trivial.
rewrite H1.
transitivity (p - 0).
apply B01_fondamental.
compute.
intros.
inversion_clear H2.
split.
trivial.
apply Rle_trans with p.
trivial.
trivial.
trivial.
apply Rminus_0_r.
apply (tech1 p H H0).
Qed.


Theorem Ens_geom_n_proba : 
forall p : R,
0 <= p -> p <= 1 ->
forall n : nat,
Ef_mesure (Ens_geom_n p n) = (1 - p) ^ n * p
.
intros.
induction n.
compute.
rewrite Rmult_1_l.
rewrite <- Bernoulli1.
2 : split ; [trivial | trivial].
assert (
 ( (fun f : Flot =>
   match f with
   | eps :: f' => (eps < p \/ eps = p) /\ Full_set Flot f'
   end): Ensemble Flot) =
fun s : Flot =>
   exists eps : Element_flot, (exists s' : Flot, s = eps :: s' /\ eps <= p)
).
apply Extensionality_Ensembles.
split.
compute.
intro.
case x.
intros.
inversion_clear H1.
exists e.
exists f.
split.
trivial.
trivial.
compute.
intros.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
subst.
split.
trivial.
apply Full_intro.
rewrite <- H1.
trivial.

unfold Ens_geom_n.
fold Ens_geom_n.
rewrite Flot_mesure_rectangle.
3 : apply Ens_geom_n_rectangle ; [trivial | trivial].
unfold not.
rewrite (Rmult_comm ((1 - p) ^ S n)).
rewrite IHn.
assert (
  Complement Element_flot (fun x => x <= p) =
  fun x : Element_flot => x <= p -> False
).
apply Extensionality_Ensembles.
split.
compute.
intuition.
compute.
intuition.
rewrite <- H1.
generalize (Proba_compl _ Espace_elem_flot Eef_mesure (fun x => x <= p) Eef_mesure_proba).
intros.
rewrite (H2 (tech1 p H H0)).
rewrite tech2.
unfold pow.
fold pow.
rewrite <- (Rmult_assoc (1 - p)).
rewrite (Rmult_comm p).
trivial.
trivial.
trivial.
assert (
  Complement Element_flot (fun x => x <= p) =
  fun x : Element_flot => ~ x <= p
).
apply Extensionality_Ensembles.
split.
compute.
intuition.
compute.
intuition.
rewrite <- H1.
unfold Espace_elem_flot.
unfold B01.
unfold Boreliens.
rewrite <- (sigma_est_sigma2).
apply sigma_complement.
rewrite sigma_est_sigma2.
apply tech1.
trivial.
trivial.
Qed.