Require Import Wf_nat. Load lo_axiom. (* Proba Caml (ALICE) version 0.091 *) (* Quelques axiomes que l'on montrera plus tard. *) Axiom Cn0 : forall n:nat, C n 0 = 1. Section Prog. Variable bernoulli : (R ->> (o bool)). Variable binomial : (R ->> (nat ->> (o nat))). Hypothesis Hyp_binomial : ((Terminaison_triangle binomial (fun p_0 => ((forall f_3, (Terminaison_triangle f_3 (fun a_18 => ((f_3 = bernoulli) /\ (a_18 = p_0))))) /\ (forall f_4, (Terminaison_triangle f_4 (fun a_19 => ((forall f_3, (Terminaison_triangle f_3 (fun a_18 => ((f_3 = bernoulli) /\ (a_18 = p_0))))) /\ (((Terminaison_triangle f_4 (fun berp_0 => True)) /\ (f_4 |> fun berp_0 y_22 => ((Terminaison_triangle y_22 (fun n_0 => ((forall b_17 : bool, True) /\ (Terminaison_triangle y_22 (fun m_2 => ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Lt) berp_0 p_0 bernoulli m_2 n_0)))))) /\ (y_22 |> fun n_0 y_21 => (exists b_17, ((exists u_0, (exists v_0, (((u_0 = n_0) /\ (v_0 = (Zero))) /\ (b_17 = true <-> (u_0 = v_0))))) /\ (((b_17 = true) -> ((Terminaison_carre y_21 (fun s_0 => True)) /\ (y_21 [] fun s_0 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_0))))) /\ ((b_17 = false) -> ((Terminaison_carre y_21 (fun s_1 => (((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ (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 x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ ((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16)))))))))) /\ (forall m_0, (((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ (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 x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ ((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16)))))))))) -> ((exists f_1, (exists a_16, (((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16))))) /\ (a_16 -- f_1 --> m_0)))) -> ((exists x_5, (exists s_2, {s_1 >> m_0 ~> x_5 >> s_2})) /\ (forall x_5, (forall s_2, ({s_1 >> m_0 ~> x_5 >> s_2} -> (forall m_1, ((m_1 = berp_0) -> ((exists b_15, (exists s_3, {s_2 >> m_1 ~> b_15 >> s_3})) /\ (forall b_15, (forall s_3, ({s_2 >> m_1 ~> b_15 >> s_3} -> (forall b_16, ((b_16 = b_15) -> ((b_16 = true) -> (forall f_2, (Terminaison_triangle f_2 (fun a_17 => (((Terminaison_triangle f_2 (fun x_1 => True)) /\ (f_2 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_17 = x_5)))))))))))))))))))))))) /\ (y_21 [] fun s_1 y_20 t_1 => (exists m_0, ((exists f_1, (exists a_16, (((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16))))) /\ (a_16 -- f_1 --> m_0)))) /\ (exists x_5, (exists s_2, ({s_1 >> m_0 ~> x_5 >> s_2} /\ (exists m_1, ((m_1 = berp_0) /\ (exists b_15, (exists s_3, ({s_2 >> m_1 ~> b_15 >> s_3} /\ ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> (exists f_2, (exists a_17, ((((Terminaison_triangle f_2 (fun x_1 => True)) /\ (f_2 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_17 = x_5)) /\ (a_17 -- f_2 --> y_20))))) /\ ((b_16 = false) -> (y_20 = x_5))))) /\ (t_1 = s_3)))))))))))))))))))))) /\ (exists f_3, (exists a_18, (((f_3 = bernoulli) /\ (a_18 = p_0)) /\ (a_18 -- f_3 --> a_19)))))))))))) /\ (binomial |> fun p_0 y_23 => (exists f_4, (exists a_19, ((((Terminaison_triangle f_4 (fun berp_0 => True)) /\ (f_4 |> fun berp_0 y_22 => ((Terminaison_triangle y_22 (fun n_0 => ((forall b_17 : bool, True) /\ (Terminaison_triangle y_22 (fun m_2 => ((fun (berp : (o bool)) (p : R) (bernoulli : (R ->> (o bool))) => Lt) berp_0 p_0 bernoulli m_2 n_0)))))) /\ (y_22 |> fun n_0 y_21 => (exists b_17, ((exists u_0, (exists v_0, (((u_0 = n_0) /\ (v_0 = (Zero))) /\ (b_17 = true <-> (u_0 = v_0))))) /\ (((b_17 = true) -> ((Terminaison_carre y_21 (fun s_0 => True)) /\ (y_21 [] fun s_0 y_19 t_0 => ((y_19 = (Zero)) /\ (t_0 = s_0))))) /\ ((b_17 = false) -> ((Terminaison_carre y_21 (fun s_1 => (((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ (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 x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ ((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16)))))))))) /\ (forall m_0, (((forall f_0, (Terminaison_triangle f_0 (fun a_15 => (((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ (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 x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0))))) /\ ((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16)))))))))) -> ((exists f_1, (exists a_16, (((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16))))) /\ (a_16 -- f_1 --> m_0)))) -> ((exists x_5, (exists s_2, {s_1 >> m_0 ~> x_5 >> s_2})) /\ (forall x_5, (forall s_2, ({s_1 >> m_0 ~> x_5 >> s_2} -> (forall m_1, ((m_1 = berp_0) -> ((exists b_15, (exists s_3, {s_2 >> m_1 ~> b_15 >> s_3})) /\ (forall b_15, (forall s_3, ({s_2 >> m_1 ~> b_15 >> s_3} -> (forall b_16, ((b_16 = b_15) -> ((b_16 = true) -> (forall f_2, (Terminaison_triangle f_2 (fun a_17 => (((Terminaison_triangle f_2 (fun x_1 => True)) /\ (f_2 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_17 = x_5)))))))))))))))))))))))) /\ (y_21 [] fun s_1 y_20 t_1 => (exists m_0, ((exists f_1, (exists a_16, (((f_1 = y_22) /\ (exists f_0, (exists a_15, ((((Terminaison_triangle f_0 (fun x_0 => True)) /\ (f_0 |> fun x_0 y_1 => (y_1 = (Pred x_0)))) /\ (a_15 = n_0)) /\ (a_15 -- f_0 --> a_16))))) /\ (a_16 -- f_1 --> m_0)))) /\ (exists x_5, (exists s_2, ({s_1 >> m_0 ~> x_5 >> s_2} /\ (exists m_1, ((m_1 = berp_0) /\ (exists b_15, (exists s_3, ({s_2 >> m_1 ~> b_15 >> s_3} /\ ((exists b_16, ((b_16 = b_15) /\ (((b_16 = true) -> (exists f_2, (exists a_17, ((((Terminaison_triangle f_2 (fun x_1 => True)) /\ (f_2 |> fun x_1 y_2 => (y_2 = (Succ x_1)))) /\ (a_17 = x_5)) /\ (a_17 -- f_2 --> y_20))))) /\ ((b_16 = false) -> (y_20 = x_5))))) /\ (t_1 = s_3)))))))))))))))))))))) /\ (exists f_3, (exists a_18, (((f_3 = bernoulli) /\ (a_18 = p_0)) /\ (a_18 -- f_3 --> a_19))))) /\ (a_19 -- f_4 --> y_23)))))) . 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_mesurable : Triangle bernoulli (fun p f => 0 <= p -> p <= 1 -> Carre f (fun _ y _ => In _ Espace_flots (fun _ => y = true)) ). Theorem Concl_binomial_termine : Double_triangle binomial (fun _ => True) (fun p binp => 0 <= p -> p <= 1 -> Double_triangle binp (fun _ => True) (fun n f => Terminaison_carre f (fun _ => True) ) ) . Proof. unfold Terminaison_triangle in Hyp_binomial. unfold Terminaison_carre in Hyp_binomial. unfold Triangle in Hyp_binomial. casser_les_cailloux. unfold Double_triangle. split. unfold Terminaison_triangle. intros. apply H. intuition. subst. intuition. compute in Hyp_bernoulli. casser_les_cailloux. apply H2. trivial. (* La terminaison du let est faite. *) unfold Triangle. unfold Double_carre. unfold Terminaison_triangle. intro. intro. intro. intros Ha_1 Ha_2. generalize (H0 a b). intuition. casser_les_cailloux. subst. generalize (H9 x0 b). intuition. clear H2. casser_les_cailloux. apply (lt_wf_ind a0). intros. apply H3. split. trivial. trivial. (* et voilà l'utilisation de la Wf-ness de Lt pour montrer d'abord que le lambda n termine. *) (* maintenant, le prob : là aussi, la Wf-ness de Lt est required. *) casser_les_cailloux. unfold Terminaison_carre. intros. subst. generalize (H9 x0 b). intuition. generalize s b0 H2. clear H2 b0 s. induction a0. intros. generalize (H10 0%nat b0 H2). intuition. casser_les_cailloux. subst. intuition. (* cas zéro est réglé *) intros. generalize (H10 (S a0) b0 H2). intuition. casser_les_cailloux. subst. generalize H8 H14 H16. case x1. intuition. intuition. generalize (H15 s). intuition. casser_les_cailloux. apply H17. intuition. intuition. subst. apply (lt_wf_ind a1). intros. apply H6. split. trivial. trivial. intuition. casser_les_cailloux. subst. generalize (H27 _ _ H25) ; intros. subst. compute in H23. apply (IHa0 s m_0). trivial. subst. compute in Hyp_bernoulli. casser_les_cailloux. generalize (H29 _ _ H7 Ha_1 Ha_2). intuition. (* La terminaison est (enfin !) prouvée. *) Qed. (* On peut (mais il est long de) montrer que : *) Axiom Concl_binomial_mesurable : Triangle binomial (fun p binp => 0 <= p -> p <= 1 -> Triangle binp (fun n f => Carre f (fun _ y _ => forall r:nat, (Le r n) -> In _ Espace_flots (fun _ => y = r) ) ) ) . Theorem Concl_binomial : Triangle binomial (fun p binp => 0 <= p -> p <= 1 -> Triangle binp (fun n f => Carre f (fun s y t => forall r:nat, (Le r n) -> Proba_locale s (y = r) = C n r * p ^ r * (1 - p) ^ (n - r) ) ) ) . unfold Terminaison_triangle in Hyp_binomial. unfold Terminaison_carre in Hyp_binomial. unfold Triangle in Hyp_binomial. casser_les_cailloux. unfold Triangle. intro. intro. intro. intros Ha_1 Ha_2. generalize (H0 a b). intro. casser_les_cailloux. generalize (H2 H1). intro. casser_les_cailloux. (* Montrons d'abord un lemme. *) assert ( forall a0 : nat, forall b0 : o nat, a0 -- b --> b0 -> forall (x : nat) (s t : Flot), { s >> b0 ~> x >> t} -> Le x a0 ). induction a0. casser_les_cailloux. subst. intros. generalize (H9 _ _ H5). intuition. generalize (H11 _ _ H3). intuition. casser_les_cailloux. subst. intuition. generalize (H18 _ _ _ H6). intuition. subst. apply le_refl. casser_les_cailloux. intros. subst. generalize (H9 _ _ H5). intuition. generalize (H11 _ _ H3). intuition. casser_les_cailloux. subst. generalize H22 H12 H20 H6. case x1. intuition. discriminate. intuition. generalize (H23 _ _ _ H10). intuition. casser_les_cailloux. subst. generalize (H30 _ _ H28). intros. compute in H21. subst. generalize (IHa0 _ H26 _ _ _ H27). intros. generalize H36 H33. case x13. intuition. casser_les_cailloux. subst. generalize (H37 _ _ H34). intros. subst. unfold Succ. apply le_n_S. trivial. intuition. subst. apply le_trans with a0. trivial. apply le_n_Sn. (* Fin du lemme. D'ailleurs, cela me donne un schéma de démonstration pour le théorème qui m'intéresse. *) unfold Carre. induction a0. casser_les_cailloux. subst. generalize (H9 _ _ H5). intuition. generalize (H10 _ _ H2). intuition. casser_les_cailloux. subst. intuition. generalize (H20 _ _ _ H11). intuition. subst. generalize (le_n_O_eq r H12). intros. subst. compute. (* replace (1 * / (1 * 1) * 1 * 1) with 1. 2 : field ; auto with real. *) rewrite Rmult_1_r. rewrite Rmult_1_l. rewrite Rmult_1_r. rewrite Rmult_1_l. rewrite Rinv_1. generalize Ef_mesure_proba. unfold Espace_proba. intuition. rewrite <- H21. rewrite <- (Proba_globale s). apply Proba_proprietes_equiv. intuition. apply Full_intro. (* Correction, Cas inductif. Le plus long. Mais on y arrivera. *) intros. casser_les_cailloux. subst. generalize (H9 _ _ H5). intuition. casser_les_cailloux. subst. intuition. generalize (H18 _ _ H14). intuition. generalize (H17 _ _ H10). intuition. casser_les_cailloux. subst. intuition. generalize H6 H24. case x4. intuition. discriminate. intuition. generalize (H25 _ _ _ H11). intuition. casser_les_cailloux. subst. inversion_clear H12. (* cas x3 = a0 ou x3 < a0 *) rewrite (pascal_step1 _ _ (le_refl (S a0))). rewrite <- minus_n_n. rewrite Cn0. rewrite Rmult_1_l. unfold pow. fold pow. rewrite Rmult_1_r. transitivity (Proba_locale s (x6 = a0 /\ x13 = true)). apply Proba_proprietes_equiv. split. intros. subst. generalize H38 H35. case x13. intuition. casser_les_cailloux. subst. generalize (H36 _ _ H33). intros. injection H31. intuition. intros. apply False_ind. (* assert False. *) intuition. subst. generalize (H3 _ _ H28). intuition. generalize (H12 _ _ _ H29). generalize (H32 _ _ H30). compute. intros. subst. generalize (le_Sn_n a0). intros. contradiction. (* contradiction. *) intuition. casser_les_cailloux. subst. apply (H36 _ _ H34). rewrite (Proba_tete_queue_indep _ _ (fun x => x = a0) (fun x => x = true) _ _ _ _ _ _ _ H29 H27). rewrite Rmult_comm. (* apply f_equal2 with (f := Rmult). *) generalize (H32 _ _ H30). intros. compute in H12. subst. rewrite (IHa0 _ H28 _ _ _ H29 a0). 2: apply le_refl. compute in Hyp_bernoulli. casser_les_cailloux. generalize (H23 _ _ H16 Ha_1 Ha_2). intuition. rewrite (H34 _ _ _ H27). rewrite (pascal_step1 _ _ (le_refl a0)). rewrite <- minus_n_n. rewrite Cn0. rewrite Rmult_1_l. assert ((1 - a) ^ 0 = 1). compute. trivial. rewrite H31. rewrite Rmult_1_r. trivial. (* Il faut encore distinguer le cas r = 0. *) generalize H23. case r. intros. rewrite Cn0. rewrite Rmult_1_l. rewrite <- minus_n_O. unfold pow. fold pow. rewrite Rmult_1_l. transitivity (Proba_locale s (x6 = 0%nat /\ x13 = false)). apply Proba_proprietes_equiv. split. intros. subst. generalize H38 H35. case x13. intros. assert False. intuition. casser_les_cailloux. subst. generalize (H39 _ _ H36). intros. discriminate. contradiction. intuition. intuition. rewrite (Proba_tete_queue_indep _ _ (fun x => x = 0%nat) (fun x => x = false) _ _ _ _ _ _ _ H29 H27). rewrite Rmult_comm. generalize (H32 _ _ H30). intros. compute in H31. subst. rewrite (IHa0 _ H28 _ _ _ H29 0%nat). 2: apply H12. compute in Hyp_bernoulli. casser_les_cailloux. generalize (H33 _ _ H16 Ha_1 Ha_2). intuition. rewrite (Proba_globale x7 (fun _ => x13 = false)). assert (Complement Flot (fun _ => x13 = true) = fun _ => x13= false). apply Extensionality_Ensembles. split. compute. case x13. intuition. trivial. compute. intros. subst. discriminate. rewrite <- H34. rewrite (Proba_compl _ Espace_flots). rewrite <- (Proba_globale x7). rewrite (H37 _ _ _ H27). rewrite <- minus_n_O. rewrite Cn0. rewrite Rmult_1_l. assert (a ^ 0 = 1). compute. trivial. rewrite H39. rewrite Rmult_1_l. trivial. apply Ef_mesure_proba. unfold Carre in Hyp_bernoulli_mesurable. unfold Triangle in Hyp_bernoulli_mesurable. apply (Hyp_bernoulli_mesurable _ _ H16 Ha_1 Ha_2 _ _ _ H27). (* Cas plus général : r <= a0. *) intros. transitivity (Proba_locale s ((x3 = S n /\ x13 = true) \/ (x3 = S n /\ x13 = false))). apply Proba_proprietes_equiv. split. intros. case x13. intuition. intuition. intuition. rewrite (Proba_globale s (fun _ => x3 = S n /\ x13 = true \/ x3 = S n /\ x13 = false) ). generalize Ef_mesure_proba. unfold Espace_proba. unfold Espace_mesurable. unfold Sigma_algebre. intuition. generalize (mesure_denomb_additive_est_additive _ _ _ H33 H31 H39 ). intros. unfold Mesure_additive in H36. generalize (Stabilite_intersection _ Espace_flots). intros. rewrite <- (Fonct_union Flot (fun _ => (x3 = S n /\ x13 = true)) (fun _ => (x3 = S n /\ x13 = false))). rewrite H36. assert (Ef_mesure (fun _ => x3 = S n /\ x13 = true) = a * (C a0 n * a ^ n * (1 - a) ^ (a0 - n))). rewrite <- (Proba_globale s). transitivity (Proba_locale s (x6 = n /\ x13 = true)). apply Proba_proprietes_equiv. intuition. casser_les_cailloux. subst. generalize (H46 _ _ H44). intros. injection H41. intuition. casser_les_cailloux. subst. generalize (H46 _ _ H44). unfold Succ ; trivial. rewrite (Proba_tete_queue_indep _ _ (fun x => x = n) (fun x => x = true) _ _ _ _ _ _ _ H29 H27). rewrite Rmult_comm. compute in Hyp_bernoulli. casser_les_cailloux. generalize (H42 _ _ H16 Ha_1 Ha_2). intros. casser_les_cailloux. rewrite (H45 _ _ _ H27). generalize (H32 _ _ H30). intro. compute in H43. subst. rewrite (IHa0 _ H28 x6 s x7). trivial. trivial. apply le_trans with (S n). apply le_n_Sn. trivial. assert ( Ef_mesure (fun _ => x3 = S n /\ x13 = false) = (1 - a) * (C a0 (S n) * a ^ (S n) * (1 - a) ^ (a0 - (S n))) ). rewrite <- (Proba_globale s). transitivity (Proba_locale s (x6 = S n /\ x13 = false)). apply Proba_proprietes_equiv. intuition. rewrite (Proba_tete_queue_indep _ _ (fun x => x = S n) (fun x => x = false) _ _ _ _ _ _ _ H29 H27). rewrite Rmult_comm. compute in Hyp_bernoulli. casser_les_cailloux. generalize (H43 _ _ H16 Ha_1 Ha_2). intros. casser_les_cailloux. rewrite (Proba_globale x7 (fun _ => x13 = false)). assert (Complement Flot (fun _ => x13 = true) = fun _ => x13 = false). apply Extensionality_Ensembles. split. compute. case x13. intuition. trivial. compute. intros. subst. discriminate. rewrite <- H44. rewrite (Proba_compl _ Espace_flots). rewrite <- (Proba_globale x7). rewrite (H46 _ _ _ H27). generalize (H32 _ _ H30). intro. compute in H47. subst. rewrite (IHa0 _ H28 x6 s x7). trivial. trivial. trivial. apply Ef_mesure_proba. unfold Carre in Hyp_bernoulli_mesurable. unfold Triangle in Hyp_bernoulli_mesurable. apply (Hyp_bernoulli_mesurable _ _ H16 Ha_1 Ha_2 _ _ _ H27). rewrite H41. rewrite H42. rewrite <- (Rmult_assoc a). rewrite <- (Rmult_assoc a). rewrite (Rmult_comm a). rewrite (Rmult_assoc (C a0 n)). assert (a * a ^ n = a ^ S n). apply refl_equal. (* unfold pow. fold pow. trivial. *) rewrite H43. rewrite (Rmult_assoc (C a0 n)). rewrite <- (Rmult_assoc (1 - a)). rewrite (Rmult_comm (1 - a)). rewrite (Rmult_assoc (C a0 (S n))). rewrite (Rmult_assoc (C a0 (S n))). rewrite (Rmult_assoc (a ^ (S n))). assert ( (1 - a) * (1 - a) ^ (a0 - S n) = (1 - a) ^ S (a0 - S n) ) . apply refl_equal. (* unfold pow. fold pow. trivial. *) rewrite H44. rewrite minus_Sn_m. rewrite <- Rmult_plus_distr_r. rewrite pascal. rewrite Rmult_assoc. trivial. apply lt_le_trans with (S n). apply le_lt_n_Sm. apply le_refl. trivial. trivial. rewrite <- (Fonct_intersection Flot (fun _ => x3 = S n) (fun _ => x13 = true)). apply H40. trivial. generalize (Concl_binomial_mesurable). unfold Triangle. unfold Carre. intuition. apply (H41 _ _ H1 Ha_1 Ha_2 _ _ H10 _ _ _ H11 (S n)). apply le_trans with a0. trivial. apply le_n_Sn. unfold Carre in Hyp_bernoulli_mesurable. unfold Triangle in Hyp_bernoulli_mesurable. apply (Hyp_bernoulli_mesurable _ _ H16 Ha_1 Ha_2 _ _ _ H27). rewrite <- (Fonct_intersection Flot (fun _ => x3 = S n) (fun _ => x13 = false)). apply H40. trivial. generalize (Concl_binomial_mesurable). unfold Triangle. unfold Carre. intuition. apply (H41 _ _ H1 Ha_1 Ha_2 _ _ H10 _ _ _ H11 (S n)). apply le_trans with a0. trivial. apply le_n_Sn. assert (Complement Flot (fun _ => x13 = true) = fun _ => x13 = false). apply Extensionality_Ensembles. split. compute. case x13. intuition. trivial. compute. intros. subst. discriminate. rewrite <- H41. inversion H33. inversion H43. apply H44. unfold Carre in Hyp_bernoulli_mesurable. unfold Triangle in Hyp_bernoulli_mesurable. apply (Hyp_bernoulli_mesurable _ _ H16 Ha_1 Ha_2 _ _ _ H27). apply Disjoint_intro. compute. intuition. inversion H41. subst. inversion H42. inversion H43. subst. discriminate. Qed. (* Ho là là ! *) End Prog.