Load lo_axiom.
(* Proba Caml (ALICE) version 0.091 *)

Section Prog.

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

Hypothesis Hyp_bernoulli : 
((Terminaison_triangle bernoulli (fun p_0 => True)) /\ (bernoulli |> fun p_0 y_21 => ((Terminaison_carre y_21 (fun s_0 => (forall m_0, (((Terminaison_carre m_0 (fun s_1 => True)) /\ (m_0 [] fun s_1 y_20 t_1 => (s_1 = y_20::t_1))) -> ((exists x_5, (exists s_2, {s_0 >> m_0 ~> x_5 >> s_2})) /\ (forall x_5, (forall s_2, ({s_0 >> m_0 ~> x_5 >> s_2} -> ((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun a_10 => True)) /\ (f_0 |> fun a_10 g_10 => ((Terminaison_triangle g_10 (fun b_10 => True)) /\ (g_10 |> fun b_10 y_14 => (y_14 = true <-> (a_10 <= b_10)%R))))) /\ (a_15 = x_5))))) /\ (forall f_1, (Terminaison_triangle f_1 (fun a_16 => ((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun a_10 => True)) /\ (f_0 |> fun a_10 g_10 => ((Terminaison_triangle g_10 (fun b_10 => True)) /\ (g_10 |> fun b_10 y_14 => (y_14 = true <-> (a_10 <= b_10)%R))))) /\ (a_15 = x_5))))) /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun a_10 => True)) /\ (f_0 |> fun a_10 g_10 => ((Terminaison_triangle g_10 (fun b_10 => True)) /\ (g_10 |> fun b_10 y_14 => (y_14 = true <-> (a_10 <= b_10)%R))))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> f_1)))) /\ (a_16 = p_0))))))))))))))) /\ (y_21 [] fun s_0 y_19 t_0 => (exists m_0, (((Terminaison_carre m_0 (fun s_1 => True)) /\ (m_0 [] fun s_1 y_20 t_1 => (s_1 = y_20::t_1))) /\ (exists x_5, (exists s_2, ({s_0 >> m_0 ~> x_5 >> s_2} /\ ((exists f_1, (exists a_16, (((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun a_10 => True)) /\ (f_0 |> fun a_10 g_10 => ((Terminaison_triangle g_10 (fun b_10 => True)) /\ (g_10 |> fun b_10 y_14 => (y_14 = true <-> (a_10 <= b_10)%R))))) /\ (a_15 = x_5)) /\ (a_15 -- f_0 --> f_1)))) /\ (a_16 = p_0)) /\ (a_16 -- f_1 --> y_19)))) /\ (t_0 = s_2)))))))))))
.

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

Proof.
generalize Hyp_bernoulli.
clear Hyp_bernoulli.
unfold Double_triangle.
unfold Double_carre.
unfold Terminaison_carre.
unfold Terminaison_triangle.
unfold Carre.
unfold Triangle.
simpl.
intros.
casser_les_cailloux.
split.
intuition.
intuition.
generalize (H0 a b H1).
intuition.
apply (H6 s).
intuition.
casser_les_cailloux.
subst.
generalize (H11 x x_5).
intuition.
generalize (H16 x_5 f_1 H14).
intuition.
(* Fin de la terminaison. *)

rewrite <- Bernoulli1.
2: split; [trivial | trivial].
rewrite <- (Proba_globale s).
apply Proba_proprietes_equiv.
generalize (H0 a b H1).
intros.
casser_les_cailloux.
generalize (H7 x s t H2).
intros.
casser_les_cailloux.
subst.
generalize (H17 x1 s x2 H8).
intros.
generalize (H16 x1 x3 H14).
intros.
casser_les_cailloux.
subst.
generalize (H15 a x H12).
intros.
casser_les_cailloux.
subst.
split.
intros.
exists x1.
exists x2.
split.
trivial.
apply (H11 H5).
intros.
casser_les_cailloux.
subst.
injection H19 ; intro ; intro.
subst.
intuition.
Qed.



End Prog.