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

Section Prog.



Variable exponential : (o R).

Hypothesis Hyp_exponential : 
((Terminaison_carre exponential (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_13 => True)) /\ (f_0 |> fun a_13 g_13 => ((Terminaison_triangle g_13 (fun b_13 => True)) /\ (g_13 |> fun b_13 y_17 => (y_17 = (a_13 - b_13)%R))))) /\ (a_15 = 0%R))))) /\ (forall f_1, (Terminaison_triangle f_1 (fun a_16 => (((Terminaison_triangle f_1 (fun x_4 => (x_4 > (R0))%R)) /\ (f_1 |> fun x_4 y_11 => (y_11 = (Ln x_4)))) /\ (a_16 = x_5)))))) /\ (forall f_2, (Terminaison_triangle f_2 (fun a_17 => (((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun a_13 => True)) /\ (f_0 |> fun a_13 g_13 => ((Terminaison_triangle g_13 (fun b_13 => True)) /\ (g_13 |> fun b_13 y_17 => (y_17 = (a_13 - b_13)%R))))) /\ (a_15 = 0%R))))) /\ (forall f_1, (Terminaison_triangle f_1 (fun a_16 => (((Terminaison_triangle f_1 (fun x_4 => (x_4 > (R0))%R)) /\ (f_1 |> fun x_4 y_11 => (y_11 = (Ln x_4)))) /\ (a_16 = x_5)))))) /\ ((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun a_13 => True)) /\ (f_0 |> fun a_13 g_13 => ((Terminaison_triangle g_13 (fun b_13 => True)) /\ (g_13 |> fun b_13 y_17 => (y_17 = (a_13 - b_13)%R))))) /\ (a_15 = 0%R)) /\ (a_15 -- f_0 --> f_2)))) /\ (exists f_1, (exists a_16, ((((Terminaison_triangle f_1 (fun x_4 => (x_4 > (R0))%R)) /\ (f_1 |> fun x_4 y_11 => (y_11 = (Ln x_4)))) /\ (a_16 = x_5)) /\ (a_16 -- f_1 --> a_17)))))))))))))))))) /\ (exponential [] 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_2, (exists a_17, (((exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun a_13 => True)) /\ (f_0 |> fun a_13 g_13 => ((Terminaison_triangle g_13 (fun b_13 => True)) /\ (g_13 |> fun b_13 y_17 => (y_17 = (a_13 - b_13)%R))))) /\ (a_15 = 0%R)) /\ (a_15 -- f_0 --> f_2)))) /\ (exists f_1, (exists a_16, ((((Terminaison_triangle f_1 (fun x_4 => (x_4 > (R0))%R)) /\ (f_1 |> fun x_4 y_11 => (y_11 = (Ln x_4)))) /\ (a_16 = x_5)) /\ (a_16 -- f_1 --> a_17))))) /\ (a_17 -- f_2 --> y_19)))) /\ (t_0 = s_2)))))))))
.

Theorem Concl_exponential :
forall p : R,
Double_carre exponential (fun s => exists x, exists t, s = x::t /\ x > 0) (fun s y t => p >= 0 ->
  Proba_locale s (y >= p) = Exp (0 - p) 
 )
.
Proof.
generalize Hyp_exponential.
unfold Double_triangle.
unfold Double_carre.
unfold Terminaison_triangle.
unfold Terminaison_carre.
unfold Triangle.
unfold Carre.
intuition.
casser_les_cailloux.
apply H1.
intros.
intuition.
subst.
apply H8.
generalize (H7 _ _ _ H3).
intros.
injection H4.
intros.
subst.
trivial.
casser_les_cailloux.
subst.
generalize (H15 0 f_2).
intuition.
(* Fin de la terminaison. *)

generalize (H2 _ _ _ H3).
intros.
casser_les_cailloux.
generalize (H18 _ _ _ H6).
intros.
subst.
generalize (H17 _ _ H15).
intuition.
subst.
generalize (H14 _ _ H12).
intuition.
generalize (H13 _ _ H10).
intuition.
subst.

rewrite <- Expo1.
2: apply Rge_le ; trivial.

rewrite <- (Proba_globale (x1::x2)).
apply Proba_proprietes_equiv.
split.
intros.
exists x1.
exists x2.
split.

trivial.
trivial.
intros.
casser_les_cailloux.
injection H16.
intros.
subst.
trivial.
Qed.


End Prog.