Require Import form_prob.
Require Import Reals.
Require Import R_lemma.
Require Import RIneq.
Require Import N_lemma.
Require Import listT.


Unset Strict Implicit.
Set Implicit Arguments.

Reserved Notation "x //\ y" (at level 50, left associativity).
Reserved Notation "x \\/ y" (at level 50, left associativity).
Reserved Notation "! x " (at level 50, left associativity).
Reserved Notation "x \ y" (at level 50, left associativity).
Reserved Notation "x <=> y" (at level 50, left associativity).
Reserved Notation "x :: y" (at level 60, no associativity).
Reserved Notation "x @ y" (at level 50, no associativity).

Ltac CaseEq t := generalize (refl_equal _ t); pattern t at -1 in |- *; case t.

(*some notations *)
 Notation "x //\ y" := (EventInter _ x y).
 Notation "x \\/ y" := (EventUnion _ x y).
 Notation " ! x " := (Eventdiff _ x).
Notation "x \ y" := (ev_diff _ y x).
Notation "x <=> y" := (EquivEv _ x y).
 Notation "a :: l":=(consT a l).
Notation "a @ l":=(appT a l).

Section Proofs.
(*------------------------ essential lemmas ---------------------------------*)
(*the events are of type V*)
Variable V : Type.
(*E is the probability space *)
Variable E : listT V.

(*a condition for the list E *)
Hypothesis length_E_not_0 : lengthT E <> 0.
Lemma lgt_E : INR (lengthT E) <> 0%R.
red in |- *.
unfold not in length_E_not_0.
intros.
apply length_E_not_0.
apply INR_eq.
auto with *.
Qed.

Lemma lt_E : (0 < INR (lengthT E))%R.
assert (INR (lengthT E) <> 0%R).
apply lgt_E.
auto with *.
Qed.

Lemma lgt_inv_E : (0 < / INR (lengthT E))%R.
apply Rinv_0_lt_compat.
apply INR_neq_lt_0.
apply not_O_INR.
exact length_E_not_0.
Qed.

Lemma INR_length_E_not_0 : INR (lengthT E) <> 0%R.
apply not_O_INR.
apply length_E_not_0.
Qed.

(* Proba = length of the event *)

Definition Pr:=Proba V E.
Definition pr:=prob V E.
Definition pr_cond:=prob_cond V E.

(*--- relation orders with 0 ---*)

(* for all event M, Pr(M)<>0 => 0<INR Pr(M) *)
Lemma ax5 : forall M : Event V, pr M <> 0%R -> (0 < INR (Pr M))%R.
unfold pr;unfold prob in |- *.
intros.
apply INR_neq_lt_0.
assert (INR (Pr M) <> 0%R /\ (/ INR (lengthT E))%R <> 0%R).
apply Rmult_neq_0_reg.
exact H.
intuition.
Qed.

(*  for all event M, Pr(M)<>0->Pr(M)<>0 *)
Lemma ax1 : forall M : Event V, pr M <> 0%R -> INR (Pr M) <> 0%R.
intros.
assert (0 < INR (Pr M))%R.
apply ax5.
exact H.
auto with real.
Qed.

(*for all event L,0<=Pr(L) *)
Lemma sup_0 : forall L : Event V, 0 <= Pr L.
intros.
auto with *.
Qed.

Lemma prob_sup0 : forall a : Event V, (0 <= pr a)%R.
intros.
unfold pr;unfold prob in |- *.
apply Rle_0.
replace 0%R with (INR 0).
apply le_INR.
apply sup_0.
auto with *.
apply lt_E.
Qed.
 


(* a remplacer ds les fichiers par prob_sup0 *)
Lemma prob_ge_0 : forall L : Event V, (0 <= pr L)%R.
intros.
unfold pr;unfold prob in |- *.
rewrite Rdiv_Rmult.
replace 0%R with (0 * / INR (lengthT E))%R.
apply Rmult_le_compat; auto with *.
apply Rmult_0_l.
Qed.
(* for all event A, Pr(A)<>0 => 0<Pr(A) *)
Lemma lt_prob_0 : forall A : Event V, pr A <> 0%R -> (0 < pr A)%R.
intros.
generalize (prob_ge_0 A).
unfold Rle in |- *; intros.
elim H0.
auto.
intro.
absurd (0%R = pr A).
auto.
auto.
Qed.

(* for all event M, Pr(M)=0->Pr(M)=0 *)
Lemma proba_0_prob : forall M : Event V, Pr M = 0 -> pr M = 0%R.
unfold pr;unfold prob in |- *.
intros.
rewrite Rdiv_Rmult.
unfold Pr in H;rewrite H.
auto with *.
Qed.

(* for all event M, INR Pr(M)<>0->INR Pr(M)<>0 *)
Lemma not_prob_0 : forall M : Event V, INR (Pr M) <> 0%R -> pr M <> 0%R.
unfold pr;unfold prob in |- *; intros.
apply not_Req_0.
unfold not in |- *; intro; apply length_E_not_0; auto with *.
auto.
Qed.

(*for all event M, Pr(M)<>0 => 0<Pr(M) *)
Lemma lt_prob_not_Proba_0 : forall M : Event V, Pr M <> 0 -> (0 < pr M)%R.
unfold pr;unfold prob in |- *.
intros.
rewrite Rdiv_Rmult.
replace 0%R with (INR 0 * INR 0)%R.
apply Rmult_le_0_lt_compat.
auto with *.
auto with *.
apply ax5.
apply not_prob_0.
unfold not in |- *; intro; apply H; auto with *.
apply Rinv_0_lt_compat.
auto with *.
auto with *.
Qed.

(* for all event L, Pr(L)<= #E *)
Lemma inf_cardE : forall L : Event V, Pr L <= lengthT E.
intros.
unfold Pr ;unfold Proba.
elim E.
auto with *.
intros.
simpl in |- *.
case (event_dec V L a).
intros.
simpl in |- *.
auto with *.
intros.
auto with *.
Qed.

(*for all event M, Pr(M)<=1 *)
Lemma inf_1 : forall M : Event V, (pr M <= 1)%R.
unfold pr;unfold prob in |- *.
intros.
rewrite Rdiv_Rmult.
rewrite <- Rinv_l with (r := INR (lengthT E)).
rewrite Rmult_comm.
apply Rmult_le_compat.
assert (0 < / INR (lengthT E))%R.
apply lgt_inv_E.
auto with *.
replace 0%R with (INR 0).
apply le_INR.
apply sup_0.
auto with *.
auto with *.
apply le_INR.
apply inf_cardE.
apply not_O_INR.
apply length_E_not_0.
Qed.

(* for all event A, Pr(A)<>0 => 1<=1/Pr(A) *)
Lemma Rinv_prob_sup1 : forall A : Event V, pr A <> 0%R -> (1 <= / pr A)%R.
intros.
assert (pr A <= 1)%R.
apply inf_1.
rewrite <- Rinv_1.
apply Rge_inv_le.
auto with *.
assert ((pr A < 0)%R \/ (pr A > 0)%R).
apply Rdichotomy; auto with *.
assert (~ (pr A < 0)%R).
apply Rle_not_lt; auto with *.
apply prob_sup0.
intuition.
auto with *.
Qed. 

(* Pr(empty)=0 *)
Lemma evt_nul : Pr (empty_ev V) = 0.
unfold Pr;unfold Proba in |- *.
elim E.
auto with *.
intros.
simpl in |- *.
case (empty V a).
tauto.
intros.
try exact H.
Qed.



(* two useful lemmas of relation orders with intersection for rewriting proba*)

(* for all events A B, Pr(A//\B)<=Pr(A) *)
Lemma le_inter : forall A B : Event V, Pr (A //\ B) <= Pr A.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
auto with *.
intros.
simpl in |- *.
case (event_inter_aux V A B a).
simpl in |- *.
case (event_dec V A a).
simpl in |- *.
auto with *.
intuition.
case (event_dec V A a).
simpl in |- *.
auto with *.
auto with *.
Qed.


(* for all events A B, Pr(A//\B)<=Pr(B) *)
Lemma le_inter_r : forall A B : Event V, Pr (A //\ B) <= Pr B.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
auto with *.
intros.
simpl in |- *.
case (event_inter_aux V A B a).
simpl in |- *.
case (event_dec V B a).
simpl in |- *.
auto with *.
intuition.
case (event_dec V B a).
simpl in |- *.
auto with *.
auto with *.
Qed.

Lemma pr_le_inter:forall A B : Event V, (pr (A //\ B) <= pr B)%R.
unfold pr;unfold prob;simpl;intros.
generalize (le_inter_r A B);unfold Pr;simpl;intro.
rewrite Rdiv_Rmult;rewrite Rdiv_Rmult.
apply Rmult_le_compat;
generalize sup_0;intro;auto with * .
Qed.

(*----------------------- Lemma for rewriting -------------------------------*)



(* for all event A, Pr(A)+Pr(~A)=#E *)
Lemma proba_sum_diff_eq :
 forall A : Event V, Pr A + Pr (! A) = lengthT E.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *; intros; auto with *.
simpl in |- *; intros.
case (event_dec V A a).
case (event_diff_aux V A a).
intros; intuition.
simpl in |- *; intros; auto with *.
 case (event_diff_aux V A a).
simpl in |- *; intros; auto with *.
intros; intuition.
Qed.

(* for all event A, Pr(~A)=1-Pr(A) *)
Lemma prob_diff_eq_min_1 :
 forall A : Event V, pr (! A) = (1 - pr A)%R.
intros.
unfold pr;unfold prob in |- *.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
replace 1%R with (INR (lengthT E) * / INR (lengthT E))%R.
rewrite Rmult_comm with (r1 := INR (lengthT E)).
rewrite Rmult_comm with (r1 := INR (Pr A)).
rewrite <- Rmult_minus_distr_l.
rewrite Rmult_comm.
apply Rmult_eq_compat_l.
assert (Pr (! A) = lengthT E - Pr A).
apply plus_minus.
symmetry  in |- * .
apply proba_sum_diff_eq.
rewrite <- minus_INR.
apply eq_INR; auto with *.
apply inf_cardE.
rewrite Rmult_comm.
apply Rinv_l.
apply lgt_E.
Qed.

(* for all event A, 0<Pr(~A) => Pr(A)<1 *)
Lemma sup_0_inf_1 :
 forall A : Event V, (0 < pr (! A))%R -> (pr A < 1)%R.
intros.
rewrite prob_diff_eq_min_1 in H.
apply Rminus_lt.
replace (pr A - 1)%R with (- (1 - pr A))%R.
auto with *.
auto with *.
Qed.





(*--- rewriting lemmas with union ---*)



(* rewriting lemmas with intersection *)


(*for all events A B, Pr(A)=Pr(A//\!B)+Pr(A//\B) *) 
Lemma Prob_plus_op :
 forall A B : Event V,
 Pr A = Pr (A //\ (! B)) + Pr (A //\ B).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
intros.
simpl in |- *.
case (event_dec V A a).
case (event_inter_aux V A (! B) a).
case (event_inter_aux V A B a).
simpl in |- *.
intuition.
intuition.
simpl in |- *.
auto.
case (event_inter_aux V A B a).
simpl in |- *.
intuition.
intuition.
case (event_inter_aux V A (! B) a).
intuition.
case (event_inter_aux V A B a).
intuition.
auto.
Qed.


(*for all events L M, Pr(L)=Pr(L//\M)+Pr(L//\!M) *) 
Lemma Prob_distr :
 forall L M : Event V,
 Pr L = Pr (L //\ M) + Pr (L //\ (! M)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
auto with *.
intros.
simpl in |- *.
case (event_dec V L a).
case (event_inter_aux V L M a).
case (event_inter_aux V L (! M) a).
intros.
simpl in a0.
intuition.
intros.
simpl in |- *.
rewrite H.
auto with *.
intros.
case (event_inter_aux V L (! M) a).
intros.
simpl in a0.
simpl in |- *.
rewrite H.
auto with *.
intros.
intuition.
intros.
case (event_inter_aux V L M a).
intros.
intuition.
intros.
case (event_inter_aux V L (! M) a).
intros.
intuition.
intros.
auto with *.
Qed.


Lemma pr_distr:forall L M : Event V,
 pr L = (pr (L //\ M) + pr (L //\ (! M)))%R.
unfold pr;simpl;intros.
generalize (Prob_distr L M);unfold Pr;simpl;intro.
unfold prob;rewrite Rdiv_Rmult;rewrite Rdiv_Rmult.
rewrite H.
rewrite Rdiv_Rmult .
rewrite plus_INR.
apply Rmult_plus_distr_r.
Qed.




(*for all events A B C D, Pr((A//\B)//\(C//\D))=Pr((A//\C)//\(B//\D)) *)
Lemma inter_sym :
 forall A B C D : Event V,
 Pr ((A //\ B) //\ (C //\ D)) =
 Pr ((A //\ C) //\ (B //\ D)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto with *.
intros.
simpl in |- *.
case (event_inter_aux V (A //\ B) (C //\ D) a).
simpl in |- *.
case (event_inter_aux V (A //\ C) (B //\ D) a).
simpl in |- *.
auto with *.
simpl in |- *.
intuition.
simpl in |- *.
case (event_inter_aux V (A //\ C) (B //\ D) a).
simpl in |- *.
intuition.
simpl in |- *.
auto with *.
Qed.



(*for all events A B C, Pr((A//\B)//\C)=Pr((A//\C)//\B) *)
Lemma proba_inter_inter :
 forall A B C : Event V,
 Pr ((A //\ B) //\ C) =
 Pr ((A //\ C) //\ B).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
simpl in |- *.
intros.
case (event_inter_aux V  (A //\ B) C a).
case (event_inter_aux V (A //\ C) B a).
intros.
simpl in |- *.
auto with *.
simpl in |- *.
intuition.
case (event_inter_aux V (A //\ C) B a).
simpl in |- *.
intros.
intuition.
intros.
simpl in |- *.
auto with *.
Qed.

(* for all events A B C, Pr((A//\B)//\C)=Pr(B//\(A//\C)) *)
Lemma inter_inter_sym :
 forall A B C : Event V,
 Pr ((A //\ B) //\ C) =
 Pr (B //\ (A //\ C)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *; auto.
simpl in |- *; intros.
case (event_inter_aux V (A //\ B) C a).
case (event_inter_aux V B (A //\ C) a).
simpl in |- *; intros; auto with *.
simpl in |- *; intros; intuition.
case (event_inter_aux V  B (A //\ C) a).
simpl in |- *; intros; intuition.
simpl in |- *; intros; auto with *.
Qed.
Lemma prob_inter :
 forall A B C : Event V,
 pr ((A //\ B) //\ C) = pr (B //\ (A //\ C)).
intros.
unfold pr;unfold prob in |- *.
rewrite inter_inter_sym.
auto with *.
Qed.

(* for all events A B C, Pr((A//\B)//\C)=Pr(A//\(B//\C)) *)
Lemma inter_comm :
 forall A B C : Event V,
 Pr ((A //\ B) //\ C) =
 Pr (A //\ (B //\ C)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *; auto.
simpl in |- *; intros.
case (event_inter_aux V (A //\ B) C a).
case (event_inter_aux V A (B //\ C) a).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros; intuition.
case (event_inter_aux V A (B //\ C) a).
simpl in |- *; intros; intuition.
simpl in |- *; intros.
auto with *.
Qed.
Lemma prob_inter_comm :
 forall A B C : Event V,
 pr ((A //\ B) //\ C) = pr (A //\ (B //\ C)).
intros.
unfold pr;unfold prob in |- *.
rewrite inter_comm.
auto with *.
Qed.


(*for all events A B, Pr(A//\B)=Pr(B//\A) *)
Lemma eq_inter_sym:forall A B : Event V,Pr (A //\ B)=Pr (B //\ A).
intros.
unfold Pr;unfold Proba.
elim E.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux V A B a).
case (event_inter_aux V B A a).
simpl;intros;auto.
simpl;intros;intuition.
case (event_inter_aux V B A a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.


(*for all events A B, Pr(!A//\B)=Pr(B)-Pr(A//\B) *)
Lemma eq_proba_inter_diff:forall A B : Event V,Pr ((! A) //\ B)=Pr B-Pr (A //\ B).
intros.
rewrite eq_inter_sym.
rewrite eq_inter_sym with (A:=A).
generalize (Prob_distr B A).
intros;auto with *.
Qed.


(*for all events A B, Pr(B)=0 => Pr(A//\B)=0 *) 
Lemma inter_0 : forall A B : Event V, Pr B = 0 -> Pr (A //\ B) = 0.
intros.
assert (Pr (A //\ B) <= Pr B).
apply le_inter_r.
rewrite H in H0.
assert (0 <= Pr (A //\ B)).
apply sup_0.
auto with *.
Qed.

Lemma prob_inter_0 :
 forall A B : Event V, pr B = 0%R -> pr (A //\ B) = 0%R.
unfold pr;unfold prob in |- *.
intros.
assert (Pr (A //\ B) = 0).
apply inter_0.
rewrite Rdiv_Rmult in H.
assert (INR (Pr B) = 0%R \/ (/ INR (lengthT E))%R = 0%R).
apply Rmult_integral.
apply H.
assert ((/ INR (lengthT E))%R <> 0%R).
assert (0 < / INR (lengthT E))%R.
apply lgt_inv_E.
auto with *.
intuition.
rewrite Rdiv_Rmult.
unfold Pr in H0;rewrite H0.
rewrite Rmult_0_l.
auto with *.
Qed.


(*for all events A B, Pr(A)=0 => Pr(A//\B)=0 *) 
Lemma inter_0_l : forall A B : Event V, Pr A = 0 -> Pr (A //\ B) = 0.
intros.
assert (Pr (A //\ B) <= Pr A).
apply le_inter.
rewrite H in H0.
assert (0 <= Pr (A //\ B)).
apply sup_0.
auto with *.
Qed.

(*for all event A, Pr(A//\!A)=0 *)
Lemma prob_inter_diff :
 forall A : Event V, Pr ((! A) //\ A) = 0.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
intros.
simpl in |- *.
case (event_inter_aux V (! A) A a).
simpl in |- *.
intuition.
auto.
Qed.
 
(*for all event A, Pr(!A//\A)=0 *)
Lemma prob_inter_diff_r :
 forall A : Event V, Pr (A //\ (! A)) = 0.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
intros.
simpl in |- *.
case (event_inter_aux V A (! A) a).
simpl in |- *.
intuition.
simpl in |- *.
auto.
Qed.

(*for all event A, Pr(A/\B /\ !A/\!B)=0 *)
Lemma prob_int_diff_eq_0:forall A B:Event V,Pr ((A //\ B) //\ ((! A) //\ (! B)))=0.
unfold Pr;unfold Proba.
elim E.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux V (A //\ B)
           ((! A) //\ (! B)) a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.

Lemma pr_int_diff_eq_0:forall A B:Event V,pr ((A //\ B) //\ ((! A) //\ (! B)))=R0.
intros.
unfold pr;unfold prob.
rewrite prob_int_diff_eq_0.
rewrite Rdiv_Rmult.
auto with * .
Qed.
 





(*--- rewriting lemmas with union and intersection ---*)

(*for all events L,M, Pr(L\/M)+Pr(L/\M)=Pr(L)+Pr(M) *)
Lemma proba_union :
 forall L M : Event V,
 Pr (L \\/ M) + Pr (L //\ M) = Pr L + Pr M :>nat.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
auto with *.
intros.
simpl in |- *.
case (event_union_aux V L M a).
simpl in |- *.
intros.
case (event_dec V L a).
simpl in |- *.
intros.
case (event_dec V M a).
simpl in |- *.
intros.
case (event_inter_aux V L M a).
simpl in |- *.
intros.
auto with *.
intros.
elim n.
split.
try exact e.
try exact e0.
intros.
case (event_inter_aux V L M a).
simpl in |- *.
intros.
elim a0.
intros.
absurd (M a).
try exact n.
try exact H1.
intros.
auto with *.
intros.
case (event_inter_aux V L M a).
simpl in |- *.
intros.
case (event_dec V M a).
simpl in |- *.
intros.
elim a0.
intros.
absurd (L a).
try exact n.
try exact H0.
intros.
elim a0.
intros.
absurd (M a).
try exact n0.
try exact H1.
case (event_dec V M a).
simpl in |- *.
intros.
auto with *.
intros.
elim o.
intros.
absurd (L a).
try exact n.
try exact H0.
intros.
absurd (M a).
try exact n0.
try exact H0.
intros.
case (event_inter_aux V L M a).
case (event_dec V L a).
case (event_dec V M a).
simpl in |- *.
intros.
elim n.
auto with *.
intros.
simpl in |- *.
auto with *.
case (event_dec V M a).
simpl in |- *.
intros.
auto with *.
intros.
simpl in |- *.
elim a0.
intros.
absurd (M a).
try exact n0.
try exact H1.
case (event_dec V L a).
case (event_dec V M a).
simpl in |- *.
intros.
elim n0.
split.
try exact e0.
try exact e.
intros.
simpl in |- *.
elim n.
left.
try exact e.
case (event_dec V M a).
simpl in |- *.
intros.
elim n.
right.
try exact e.
intros.
try exact H.
Qed.


(*for all events L,M, Pr(L\/M)=Pr(L)+Pr(M)-Pr(L/\M) *) 
Lemma prob_un :
 forall L M : Event V,
 Pr (L \\/ M) = Pr L + Pr M - Pr (L //\ M) :>nat.
intros.
assert
 (Pr (L \\/ M) + Pr (L //\ M) = Pr L + Pr M :>nat).
apply proba_union.
auto with *.
Qed.


Lemma pr_union:forall A B:Event V,pr (A \\/ B)=(pr A+pr B-pr (A //\ B))%R.
intros.
unfold pr;unfold prob.
rewrite prob_un.
replace (Pr A + Pr B - Pr (A //\ B)) with 
(Pr A + (Pr B - Pr (A //\ B))).
rewrite plus_INR.
rewrite minus_INR.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
replace (INR (Pr A) + (INR (Pr B) - INR (Pr (A //\ B))))%R with
(INR (Pr A) + ((INR (Pr B) - INR (Pr (A //\ B)))))%R.
rewrite Rmult_plus_distr_r.
rewrite Rmult_comm with (r1:= (INR (Pr B) - INR (Pr (A //\ B)))%R).
rewrite Rmult_minus_distr_l.
rewrite Rmult_comm with (r1:= (/ INR (lengthT E))%R).
rewrite Rmult_comm with (r1:= (/ INR (lengthT E))%R).
ring.
auto with * .
auto with * .
apply le_inter_r.
apply plus_min_ass.
apply le_inter_r.
Qed.


(*for all events A B, Pr(A)=Pr((A//\!B)\/(A//\B)) *) 
Lemma Prob_un_op :
 forall A B : Event V,
 Pr A = Pr ((A //\ (! B)) \\/ (A //\ B)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
simpl in |- *.
intros.
case (event_dec V A a).
simpl in |- *.
case (event_union_aux V (A //\ (!B)) (A //\ B) a).
simpl in |- *.
intros.
auto.
simpl in |- *.
intros.
intuition.
case (event_union_aux V (A //\ (! B)) (A //\ B) a).
simpl in |- *.
intros.
intuition.
simpl in |- *.
auto.
Qed.


(*for all event A B C, Pr((A\/B)//\C)=Pr((A//\C)\/(B//\C)) *)
Lemma un_inter :
 forall A B C : Event V,
 Pr ((A \\/ B) //\ C) =
 Pr ((A //\ C) \\/ (B //\ C)).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
simpl in |- *.
intros.
case (event_inter_aux V (A \\/ B) C a).
simpl in |- *.
intros.
case (event_union_aux V (A //\ C) (B //\ C) a).
simpl in |- *.
intros.
auto with *.
simpl in |- *.
intros.
intuition.
simpl in |- *.
case (event_union_aux V (A //\ C) (B //\ C) a).
simpl in |- *.
intros.
intuition.
auto with *.
Qed.
Lemma prob_un_inter :
 forall A B C : Event V,
 pr ((A \\/ B) //\ C) =
 pr ((A //\ C) \\/ (B //\ C)).
intros.
unfold pr;unfold prob in |- *.
rewrite un_inter.
auto with *.
Qed.

(*for all event A B, Pr((A\/B)//\!B)=Pr(A//\!B) *)
Lemma un_inter_diff :
 forall A B : Event V,
 Pr ((A \\/ B) //\ (! B)) =
 Pr (A //\ (! B)).
intros.
rewrite un_inter.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *.
auto.
simpl in |- *.
intros.
case
 (event_union_aux V (A //\ (! B)) (B //\ (! B)) a).
case (event_inter_aux V A (! B) a).
simpl in |- *.
auto.
simpl in |- *.
intuition.
simpl in |- *.
case (event_inter_aux V A (! B) a).
simpl in |- *.
intuition.
auto.
Qed.


(* for all events A B, Pr(!A//\!B)=Pr(!(A\/B)) *)
Lemma proba_un_diff:forall A B:Event V,Pr ((! A) //\ (! B))= Pr (! (A \\/ B)).
unfold Pr;unfold Proba.
elim E.
simpl;auto.
simpl;intros.
case (event_inter_aux V (! A) (! B) a).
case (event_diff_aux V (A \\/ B) a).
simpl;intros;auto.
simpl;intros;intuition.
case (event_diff_aux V (A \\/ B) a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.
Lemma prob_un_diff:forall A B:Event V,pr ((! A) //\ (! B))= pr (! (A \\/ B)).
unfold pr;unfold prob.
intros.
rewrite proba_un_diff.
auto.
Qed.

(*for all events A B C,Pr((!A//\!B)//\C)=Pr(!(A\/B)//\C) *)
Lemma proba_inter_diff_un:forall A B C:Event V,Pr (((! A) //\ (! B)) //\ C)= Pr ((! (A \\/ B)) //\ C).
unfold Pr;unfold Proba.
elim E.
simpl;auto.
simpl;intros.
case (event_inter_aux V ((! A) //\ (! B)) C a).
case ( event_inter_aux V (! (A \\/ B)) C a).
simpl;intros;auto.
simpl;intros;intuition.
case ( event_inter_aux V (! (A \\/ B)) C a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.
Lemma prob_inter_diff_un:forall A B C:Event V,pr (((! A) //\ (! B)) //\ C)= pr ((! (A \\/ B)) //\ C).
unfold pr;unfold prob.
intros.
rewrite proba_inter_diff_un.
auto.
Qed.

(*--- rewriting lemmas with A \ B ---*)

(*for all events A B C, (A=>B) => Pr(A//\C)+Pr(B\A //\C)=Pr(B//\C) *)
Lemma proba_cond_ev_diff:forall A B C:Event V,(forall x:V, A x->B x)->Pr (A //\ C) +Pr ((B \ A) //\ C)=
   Pr (B //\ C).
unfold Pr;unfold Proba.
elim E.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux V A C a).
case (event_inter_aux V (B \ A) C a).
case (event_inter_aux V B C a).
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros.
case (event_inter_aux V B C a).
simpl;intros.
auto with * . 
simpl;intros.
assert (~ event_pred V A a). 
intuition.
intuition.
case (event_inter_aux V (B \ A) C a).
case (event_inter_aux V B C a).
simpl;intros.
rewrite <-plus_n_Sm. 
rewrite H.
auto with * .
auto.
simpl;intros;intuition.
case (event_inter_aux V B C a).
simpl;intros.
intuition.
simpl;intros.
apply H.
auto.
Qed.

(*--  probabilities with implication ---*)

Definition filt:=filter V.

(*for all events A B C, for all list l, 
(for all x:V,A x => B x) => subListT V (filt A l) (filt B l) *)
Lemma prob_impl1 :
 forall (A B : Event V) (l : listT V),
 (forall x : V, A x -> B x) -> subListT V (filt A l) (filt B l).
intros.
induction  l as [| a l Hrecl].
simpl in |- *.
auto.
simpl in |- *.
case (event_dec V A a).
case (event_dec V B a).
simpl in |- *.
auto with *.
intros.
absurd (B a).
exact n.
auto with *.
case (event_dec V B a).
intros.
generalize Hrecl.
case (filt A l).
simpl in |- *.
auto.
simpl in |- *.
intuition.
intuition.
Qed.

(*for all A:Type,for all a:A, for all list l1 l2, 
sublistT A (a :: l1) l2 => subListT V (filt A l) (filt B l) *)
Lemma prob_impl2 :
 forall (A : Type) (a : A) (l1 l2 : listT A),
 subListT A (a :: l1) l2 -> subListT A l1 l2.
clear length_E_not_0.
simple induction l2.
simpl in |- *.
intuition.
induction  l1 as [| a0 l1 Hrecl1].
intros.
simpl in |- *.
auto.
clear l2.
intros.
rename a1 into b.
rename a into a1.
rename a0 into a2.
rename l into l2.
simpl in |- *.
elim H0.
intuition.
constructor 2.
apply H.
exact H1.
Qed.

(*for all A:Type, for all list l1 l2, 
sublistT A l1 l2 => #l1 <= #l2 *)
Lemma prob_impl3 :
 forall (A : Type) (l1 l2 : listT A),
 subListT A l1 l2 -> lengthT l1 <= lengthT l2.
simple induction l1.
simpl in |- *.
auto with *.
clear l1 length_E_not_0.
simple induction l2.
simpl in |- *.
intuition.
intros.
rename l into l1.
rename a0 into b.
clear l2.
rename l0 into l2.
simpl in |- *.
assert (lengthT l1 <= lengthT l2).
apply H.
elim H1.
intuition.
apply prob_impl2.
auto with *.
Qed.

(* for all events e1 e2, (e1=>e2) => Pr(e1)<=Pr(e2) *)
Lemma prob_impl :
 forall e1 e2 : Event V, (forall x : V, e1 x -> e2 x) -> (pr e1 <= pr e2)%R.
intros.
unfold pr ;unfold prob.
unfold Pr;unfold Proba in |- *.
apply Rdiv_Rle.
apply INR_neq_lt_0.
apply not_O_INR.
apply length_E_not_0.
apply le_INR.
apply prob_impl3.
apply prob_impl1.
exact H.
Qed.


(*for all event A B C, (A =>B) => Pr(A | C) <= Pr(B | C) *)
Lemma pr_cond_impl_aux :
 forall A B C : Event V,
 (0 < pr C)%R ->
 (forall x : V, A x -> B x) -> (pr_cond A C <= pr_cond B C)%R.
intros.
unfold pr_cond;unfold prob_cond.
apply Rle_inv_monotony_r.
exact H.
apply prob_impl.
intros x.
assert (A x -> B x).
auto.
simpl in |- *.
intuition.
Qed.
Lemma pr_cond_impl :
 forall A B C : Event V,
 (forall x : V, A x -> B x) -> (pr_cond A C <= pr_cond B C)%R.
intros.
case (dec_eq_nat (Pr C) 0).
intros.
unfold pr_cond;unfold prob_cond.
unfold pr ;unfold prob.
rewrite inter_0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
rewrite inter_0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
auto with *.
auto.
auto.
intros.
apply pr_cond_impl_aux.
apply lt_prob_not_Proba_0.
auto.
auto.
Qed.

(*--- rewriting lemmas with A<=>B ---*)

(* for all events e1 e2, (e1<=>e2) => Pr(e1)=Pr(e2) *)
Lemma prob_equiv :
 forall e1 e2 : Event V, (forall x : V, e1 x <-> e2 x) -> pr e1 = pr e2.
intros.
apply Rle_antisym.
apply prob_impl.
intros.
assert (e1 x <-> e2 x).
apply H.
intuition.
apply prob_impl.
intros.
assert (e1 x <-> e2 x).
apply H.
intuition.
Qed.


(* for all events e1 e2 e3, (e1<=>e2) => e3//\e1 <=> e3//\e2 *)
Lemma equiv_inter: forall e1 e2 e3 : Event V, (forall x : V, e1 x <-> e2 x)->(forall x : V,(e3 //\ e1) x <-> (e3 //\ e2) x).
intros.
simpl.
generalize (H x).
intro;intuition.
Qed.

(* for all events e1 e2 e3, (e1<=>e2) => pr (e3//\e1)=pr (e3//\e2) *)
Lemma prob_equiv_inter: forall e1 e2 e3 : Event V, (forall x : V, e1 x <-> e2 x)->pr (e3 //\ e1)=pr (e3 //\ e2).
intros.
apply Rle_antisym.
apply prob_impl.
intros.
generalize (equiv_inter e3 H ).
intro.
generalize (H1 x).
intros.
intuition.
apply prob_impl.
intros.
generalize (equiv_inter e3 H).
intro;generalize (H1 x).
intros.
intuition.
Qed.

(* for all events A B, (A<=>B) => pr (A<=>B)=pr (A/\B \/ !A/\B) *)
Lemma prob_equiv_ev:forall A B:Event V,Pr (A<=> B)=Pr ((A //\ B) \\/ ((! A) //\ (! B))).
unfold Pr;unfold Proba.
elim E.
simpl;intros;auto.
simpl;intros.
case (dec_pred_equiv V A B (ev_dec V A) (ev_dec V B) a).
case (event_union_aux V (A //\ B)
           ((! A) //\ (! B)) a).
simpl;intros;auto.
simpl;intros;intuition.
simpl;intros.
case (event_union_aux V (A //\ B)
           ((! A) //\ (! B)) a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.

Lemma pr_equiv:forall A B:Event V,pr (A <=> B)=pr ((A //\ B) \\/ ((! A) //\ (! B))).
unfold pr;unfold prob.
intros.
rewrite prob_equiv_ev.
auto.
Qed.

(* for all events A B, pr (A /\ (A<=>B))=pr (A/\B) *)
Lemma prob_int_equiv:forall A B:Event V,Pr (A //\ (A <=> B))=Pr (A //\ B).
unfold Pr;unfold Proba.
elim E.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux V A (A <=> B) a).
case (event_inter_aux V A B a).
simpl;intros;auto.
simpl;intros;intuition.
case (event_inter_aux V A B a).
simpl;intros;intuition.
simpl;intros;auto.
Qed.

Lemma pr_int_equiv:forall A B:Event V,pr (A //\ (A <=> B))=pr (A //\ B).
unfold pr;unfold prob.
intros.
rewrite prob_int_equiv.
auto.
Qed.

(* for all events A B, pr (A | A<=>B)=pr (A/\B) / pr (A/\B \/ !A/\!B) *)
Lemma pr_cond_equiv:forall A B:Event V,pr_cond  A (A <=> B)=(pr (A //\ B)/(pr ((A //\ B) \\/ ((! A) //\ (! B)))))%R.
unfold pr_cond;unfold prob_cond.
simpl;intros.
rewrite pr_int_equiv.
rewrite pr_equiv.
auto.
Qed.

(* for all events A B C, B<=>C -> pr (A | B)=pr (A/\B) / pr (A | C) *)
Lemma  pr_cond_equiv2 :
    forall A B C : Event V ,
    (forall x : V, B x <-> C x) -> pr_cond A B = pr_cond A C.
unfold pr_cond;unfold prob_cond.
intros.
generalize (prob_equiv H);unfold pr;intro heq;rewrite heq;auto.
generalize (prob_equiv_inter A H);unfold pr;intro h;rewrite h;auto.
Qed.


(*--- rewriting lemmas with conditionnal probability ---*)

(* 0 <= pr (A | B) *)
Lemma prob_cond_sup0 : forall A B : Event V, (0 <= pr_cond A B)%R.
intros.
assert ({pr B = 0%R} + {pr B <> 0%R}).
apply Aeq_dec.
case H.
unfold pr_cond;unfold prob_cond in |- *.
intros.
rewrite Rdiv_Rmult.
assert (pr (A//\ B) = 0%R).
unfold pr;unfold prob in |- *.
rewrite Rdiv_Rmult.
assert (Pr (A//\B) = 0).
apply inter_0; auto with * .
unfold pr in e;unfold prob in e.
rewrite Rdiv_Rmult in e.
assert (INR (Pr B) = INR 0).
apply Req_0 with (b := INR (lengthT E)).
apply lgt_E.
auto with * .
apply INR_eq; auto with * .
unfold Pr in H0;rewrite H0.
auto with * .
unfold pr in H0;rewrite H0.
auto with * .
intros.
unfold pr_cond;unfold prob_cond in |- *.
apply Rle_0.
apply prob_sup0.
assert ((pr B < 0)%R \/ (pr B > 0)%R).
apply Rdichotomy.
auto with * .
assert (~ (pr B < 0)%R).
apply Rle_not_lt; auto with * .
apply prob_sup0.
intuition.
Qed.

(* for all events A B, Pr(A//\B)=Pr(A | B)*Pr(B) *)
Lemma pr_cond_eq :
 forall A B : Event V, pr (A //\ B) = (pr_cond A B * pr B)%R.
intros.
assert ({pr B = 0%R} + {pr B <> 0%R}).
apply Aeq_dec with (x := pr B) (y := 0%R).
case H.
intros.
rewrite e.
assert (pr (A //\ B) = 0%R).
unfold pr in |- *.
assert (Pr (A //\ B) = 0).
apply inter_0.
unfold pr in e.
unfold prob in e.
rewrite Rdiv_Rmult in e.
assert (INR (Pr B) = 0%R \/ (/ INR (lengthT E))%R = 0%R).
apply Rmult_integral.
apply e.
assert ((/ INR (lengthT E))%R <> 0%R).
assert (0 < / INR (lengthT E))%R.
apply lgt_inv_E.
auto with *.
intuition.
unfold prob;rewrite Rdiv_Rmult.
unfold Pr in H0;rewrite H0.
auto with *.
rewrite Rmult_0_r.
auto with *.
intros.
unfold pr_cond;unfold prob_cond in |- *.
unfold prob.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
rewrite Rinv_l.
auto with *.
auto with *.
Qed.


(* for all events A B, Pr(A)=Pr(A | B)*Pr(B)+Pr(A | !B)*Pr(!B) *)
Lemma prob_eq_cond :
 forall A B : Event V,
 pr A =
 (pr_cond A B * pr B + pr_cond A (! B) * pr (! B))%R.
intros.
rewrite <- pr_cond_eq.
rewrite <- pr_cond_eq.
unfold pr;unfold prob in |- *.
generalize (Prob_distr A B);unfold Pr;intro heq;rewrite heq.
rewrite plus_INR.
rewrite Rdiv_Rmult.
rewrite Rmult_plus_distr_r.
auto with *.
Qed.


(*for all events A B C, (A=>B) => Pr(A | C)+Pr(B\A | C)=Pr(B | C) *)
Lemma pr_cond_ev_diff:forall A B C:Event V,(forall x:V, A x->B x)->((pr_cond A C)+(pr_cond (B \ A) C))%R=pr_cond B C.
intros.
unfold pr_cond;unfold prob_cond.
case (dec_eq_nat (Pr C) 0).
intro.
unfold pr;unfold prob.
rewrite inter_0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
rewrite inter_0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
rewrite inter_0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
auto with * .
auto.
auto.
auto.
auto.
intro.
rewrite <-Rdiv_Rplus_eq.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply eq_Rmult.
unfold pr;unfold prob.
rewrite <-Rdiv_Rplus_eq.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply eq_Rmult.
rewrite <-plus_INR.
apply eq_INR.
apply proba_cond_ev_diff.
auto.
auto.
intro.
apply length_E_not_0.
auto with * .
auto.
unfold pr;unfold prob.
intro.
apply H0.
apply INR_eq.
apply Req_0 with (INR (lengthT E)). 
intro.
apply length_E_not_0.
auto with * .
auto.
Qed.

(*for all events A B C, Pr(A//\B | C)=Pr(B//\A | C) *)
Lemma pr_cond_inter_sym:forall (A B C:Event V ),pr_cond  (A //\ B) C=pr_cond  (B //\ A) C.
intros.
unfold pr_cond;unfold prob_cond.
rewrite prob_equiv with (e2:=((B //\ A) //\ C)).
auto.
simpl;intuition.
Qed.

(* for all events A B C, Pr(B//\C)<>0 => Pr(A//\B | C)=Pr(A | B//\C)*Pr(B | C) *)
Lemma pr_cond_mult :
 forall A B C : Event V,
 pr (B //\ C) <> 0%R ->
 pr_cond (A //\ B) C =
 (pr_cond A (B //\ C) * pr_cond B C)%R.
intros.
unfold pr_cond ;unfold prob_cond.
rewrite prob_inter_comm.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
replace (prob V E (A //\ (B //\ C)) *
 (/ prob V E (B //\ C) * (prob V E (B //\ C) * / prob V E C)))%R
with 
(prob V E (A //\ (B //\ C)) *
 (/ prob V E (B //\ C) * prob V E (B //\ C)) * / prob V E C)%R.
rewrite (Rinv_l (prob V E (B //\ C))).
rewrite Rmult_1_r.
auto with *.
auto with *.
rewrite Rmult_assoc.
auto with *.
Qed.



(*for all events A B C, Pr(A//\C)<>0 =>Pr(A//\B | C)=Pr(B | A//\C)*Pr(A | C) *)
Lemma pr_cond_mult_ :
 forall A B C : Event V,
 pr (A //\ C) <> 0%R ->
 pr_cond (A //\ B) C =
 (pr_cond B (A //\ C) * pr_cond A C)%R.
intros.
unfold pr_cond;unfold prob_cond in |- *.
rewrite prob_inter.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
replace (prob V E (B //\ (A //\ C)) *
 (/ prob V E (A //\ C) * (prob V E (A //\ C) * / prob V E C)))%R
with
(prob V E (B //\ (A //\ C)) *
 (/ prob V E (A //\ C) * prob V E (A //\ C)) * / prob V E C)%R.
rewrite (Rinv_l (prob V E (A //\ C))).
rewrite Rmult_1_r.
auto with *.
auto with *.
rewrite Rmult_assoc.
auto with *.
Qed.

(*for all events A B C, Pr(A//\B | C)=Pr(B | A//\C)*Pr(A | C) *)
Lemma pr_cond_mult_r: forall A B C : Event V,
 pr_cond (A //\ B) C =
 (pr_cond B (A //\ C) * pr_cond A C)%R.
intros.
case (dec_eq_nat (Pr (A //\ C)) 0).
intro.
unfold pr_cond;unfold prob_cond.
unfold prob.
rewrite inter_inter_sym.
rewrite inter_0.
unfold Pr in H;rewrite H.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
rewrite Rdiv_Rmult.
rewrite Rmult_0_r.
auto.
auto.
intro.
apply pr_cond_mult_.
apply not_prob_0.
auto with * .
Qed.


(* for all events L M N, Pr(N)<>0 => Pr(L | N)=Pr(L//\M | N)+Pr(L//\!M | N) *)
Lemma pr_cond_distr :
 forall L M N : Event V,
 pr N <> 0%R ->
 pr_cond L N =
 (pr_cond (L //\ M) N + pr_cond (L //\ (! M)) N)%R.
intros.
unfold pr_cond;unfold prob_cond in |- *.
unfold pr;unfold prob in |- *.
rewrite Rdiv_Rdiv.
rewrite Rdiv_Rdiv.
rewrite Rdiv_Rdiv.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rplus_mult.
assert
 (INR (Pr (L //\ N)) =
  (INR (Pr ((L //\ M) //\ N)) +
   INR (Pr ((L //\ (! M))//\ N)))%R).
rewrite proba_inter_inter.
rewrite proba_inter_inter with (B := ! M).
assert
 (Pr (L //\ N) =
  Pr ((L //\ N) //\ M) +
  Pr ((L //\ N) //\ (! M))).
apply Prob_distr with (L := L //\ N) (M := M).
apply Rmult_eq with (b := INR (Pr N)).
unfold pr;unfold prob in H.
assert (INR (Pr N) <> 0%R).
apply Rlt_0 with (b := INR (lengthT E)).
auto with *.
assert (lengthT E <> 0).
apply length_E_not_0.
auto with *.
auto with *.
rewrite H0.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite plus_INR.
auto with *.
unfold Pr in H0;rewrite H0.
auto with *.
auto with *.
unfold pr;unfold prob in H.
replace (0 < INR (Pr N))%R with (INR 0 < INR (Pr N))%R.
assert (INR 0 <= INR (Pr N))%R.
apply le_INR.
apply sup_0.
assert (INR (Pr N) <> INR 0).
apply Rlt_0 with (b := INR (lengthT E)).
auto with *.
assert (lengthT E <> 0).
apply length_E_not_0.
auto with *.
assert (~ (INR (Pr N) < INR 0)%R).
apply Rle_not_lt.
auto with *.
assert ((INR (Pr N) < INR 0)%R \/ (INR (Pr N) > INR 0)%R).
apply Rdichotomy.
auto with *.
intuition.
auto with *.
auto with *.
unfold pr;unfold prob in H.
replace (0 < INR (Pr N))%R with (INR 0 < INR (Pr N))%R.
assert (INR 0 <= INR (Pr N))%R.
apply le_INR.
apply sup_0.
assert (INR (Pr N) <> INR 0).
apply Rlt_0 with (b := INR (lengthT E)).
auto with *.
assert (lengthT E <> 0).
apply length_E_not_0.
auto with *.
assert (~ (INR (Pr N) < INR 0)%R).
apply Rle_not_lt.
auto with *.
assert ((INR (Pr N) < INR 0)%R \/ (INR (Pr N) > INR 0)%R).
apply Rdichotomy.
auto with *.
intuition.
auto with *.
auto with *.
unfold pr;unfold prob in H.
replace (0 < INR (Pr N))%R with (INR 0 < INR (Pr N))%R.
assert (INR 0 <= INR (Pr N))%R.
apply le_INR.
apply sup_0.
assert (INR (Pr N) <> INR 0).
apply Rlt_0 with (b := INR (lengthT E)).
auto with *.
assert (lengthT E <> 0).
apply length_E_not_0.
auto with *.
assert (~ (INR (Pr N) < INR 0)%R).
apply Rle_not_lt.
auto with *.
assert ((INR (Pr N) < INR 0)%R \/ (INR (Pr N) > INR 0)%R).
apply Rdichotomy.
auto with *.
intuition.
auto with *.
Qed.

(* for all events A B C, pr (A/\B | C)=pr (B | A/\C) * pr (A | C) *)
Lemma pr_cond_int1 :
    forall A B C : Event V ,
    pr_cond (A //\ B) C =
    (pr_cond B (A //\ C) * pr_cond A C)%R.
unfold pr_cond;unfold prob_cond.
intros.
case (dec_eq_nat (Proba  V E (A //\ C)) (0)).
intros.
unfold prob.
rewrite inter_inter_sym.
rewrite inter_0.
rewrite H;simpl.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite RIneq.Rmult_0_l.
rewrite RIneq.Rmult_0_l.
rewrite RIneq.Rmult_0_r.
auto.
auto.

intro.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
replace (prob V E (B //\ (A //\ C)) *
    / prob V E (A //\ C) *
    (prob V E (A //\ C) * / prob V E C))%R with (pr (B //\ (A //\ C)) *
    (/ pr (A //\ C) *
    (pr (A //\ C) )* / pr C))%R.
rewrite Rinv_l.
rewrite Rmult_1_l.
unfold prob.
generalize inter_inter_sym;unfold Pr;simpl;intro heq.
rewrite heq.
auto.
apply not_prob_0;auto.
unfold not;intro;unfold not in H;apply H.
apply RIneq.INR_eq.
auto.
rewrite Rmult_assoc.
auto with *.
Qed.

(*---------------------- independance of probabilities --------------------- *)

Definition Indep:=indep V E.

Lemma indep_diff1 : forall A B : Event V, Indep A B -> Indep(! A) B.
unfold Indep;unfold indep.
intros A B H.
rewrite prob_diff_eq_min_1.
unfold prob.
simpl;intros.
rewrite eq_proba_inter_diff.
rewrite R_lemma.Rminus_distr_div.
unfold prob in H.
unfold Pr;rewrite H.
rewrite R_lemma.one_min_mult.
auto.
apply le_inter_r.
Qed.


Lemma indep_diff2 : forall A B : Event V, Indep A B -> Indep A (! B).
unfold Indep;unfold indep.
intros A B.
rewrite prob_diff_eq_min_1.
unfold prob.
simpl;intros.
rewrite eq_inter_sym.
rewrite eq_proba_inter_diff.
rewrite Rminus_distr_div.
rewrite eq_inter_sym in H.
rewrite H.
rewrite Raxioms.Rmult_comm with (r1:= (Rdefinitions.Rdiv (Raxioms.INR (Pr A)) (Raxioms.INR (lengthT E)))).
rewrite  Raxioms.Rmult_comm with (r1:= (Rdefinitions.Rdiv (Raxioms.INR (Pr A)) (Raxioms.INR (lengthT E)))).
rewrite one_min_mult.
auto.
apply le_inter_r.
Qed.

Lemma indep_diff3: forall A B : Event V, Indep A B -> Indep (! A) (! B).
intros.
apply indep_diff2.
apply indep_diff1.
auto.
Qed.

(* Indep A B -> pr (A | B)= pr A *)
Lemma indep_cond :
 forall A B : Event V,
 pr B <> Rdefinitions.R0 -> Indep A B -> pr_cond A B = pr A.
unfold Indep; unfold indep;unfold pr_cond ;unfold prob_cond.
intros.
rewrite H0.
rewrite Rdiv_Rmult.
rewrite  Raxioms.Rmult_assoc.
rewrite RIneq.Rinv_r.
auto with *.
auto.
Qed.

(*Indep A B -> pr (A <=> B)=pr A * pr B + pr (!A) * pr (!B) *)
Lemma pr_cond_equiv_indep:forall A B:Event V,Indep A B->pr (A <=> B)=(pr A * pr B + pr (! A) * pr (! B))%R.
unfold Indep;unfold indep.
intros.
rewrite pr_equiv.
rewrite pr_union.
unfold pr;rewrite H.
rewrite pr_int_diff_eq_0.
rewrite indep_diff3.
auto with * . 
auto.
Qed.



(*--------------------------  Relation between orders -----------------------*)


(*--- relation orders with union ---*)


(*for all events A B, Pr(A\\/B)<=Pr(A)+Pr(B) *)
Lemma le_union :
 forall A B : Event V, Pr (A \\/ B) <= Pr A + Pr B.
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *; auto with *.
simpl in |- *; intros.
case (event_union_aux V A B a).
case (event_dec V A a).
case (event_dec V B a).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
auto with *.
case (event_dec V B a).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
intuition.
case (event_dec V A a).
case (event_dec V B a).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
auto with *.
case (event_dec V B a).
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
auto with *.
Qed.


Lemma le_prob_un :
 forall A B : Event V, (pr (A \\/ B) <= pr A + pr B)%R.

intros; unfold pr;unfold prob in |- *.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite <- Rmult_plus_distr_r.
apply Rmult_le_compat.
replace 0%R with (INR 0).
apply le_INR.
apply sup_0.
auto with *.
apply Rlt_le.
apply lgt_inv_E.
rewrite <- plus_INR.
apply le_INR.
apply le_union.
auto with *.
Qed.

Lemma Rle_union :
 forall A B : Event V, (pr (A \\/ B) <= pr A + pr B)%R.
intros.
unfold pr;unfold prob in |- *.
rewrite <- plus_Rplus_div.
apply Rdiv_Rle.
apply lt_E.
apply le_INR.
apply le_union.
Qed.

(*--- relation orders with intersection ---*)

(*remplacer par le_inter_r*)
(*
Lemma length_int :
 forall (A B : Event V) (L : listT V),
 lengthT (filt (A //\ B) L) <= lengthT (filt B L).
intros.
induction  L as [| a L HrecL].
auto.
simpl in |- *.
case (event_inter_aux V A B a).
case (event_dec V B a).
simpl in |- *.
auto with *.
intuition.
case (event_dec V B a).
simpl in |- *.
auto with *.
auto with *.
Qed.
*)

(* for all events A B C, Pr(A//\B)//\C)<=Pr(B//\C) *)
Lemma le_inter_inter :
 forall A B C : Event V,
 Pr ((A //\ B) //\ C) <= Pr (B //\ C).
intros.
unfold Pr;unfold Proba in |- *.
elim E.
simpl in |- *; auto.
simpl in |- *; intros.
case (event_inter_aux V (A //\ B) C a).
case (event_inter_aux V B C a).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
case (event_inter_aux V B C a).
simpl in |- *; intros.
intuition.
auto with *.
Qed.


 (* for all events A B, Pr(A//\B)<=Pr(A)+Pr(B) *)
Lemma inter_le :
 forall A B : Event V, Pr (A //\ B) <= Pr A + Pr B.
intros.
assert (Pr (A //\ B) <= Pr A).
apply le_inter.
apply le_trans with (m := Pr A).
try exact H.
auto with *.
Qed.


(*--- relation orders with conditionnal proba ---*)


(* for all events A B, 0<=Pr(A | B) *)
Lemma pr_cond_sup0 : forall A B : Event V, (0 <= pr_cond A B)%R.
intros.
assert ({pr B = 0%R} + {pr B <> 0%R}).
apply Aeq_dec.
case H.
unfold pr_cond ;unfold prob_cond;unfold pr.
intros.
rewrite Rdiv_Rmult.
assert (pr (A //\ B) = 0%R).
unfold pr;unfold prob in |- *.
rewrite Rdiv_Rmult.
assert (Pr (A //\ B) = 0).
apply inter_0; auto with *.
unfold pr;unfold prob in e.
rewrite Rdiv_Rmult in e.
assert (INR (Pr B) = INR 0).
apply Req_0 with (b := INR (lengthT E)).
apply lgt_E.
auto with *.
apply INR_eq; auto with *.
unfold Pr in H0;rewrite H0.
auto with *.
unfold pr in H0;rewrite H0.
auto with *.
intros.
unfold pr_cond;unfold prob_cond.
apply Rle_0.
apply prob_sup0.
assert ((pr B < 0)%R \/ (pr B > 0)%R).
apply Rdichotomy.
auto with *.
assert (~ (pr B < 0)%R).
apply Rle_not_lt; auto with *.
apply prob_sup0.
intuition.
Qed.


(* for all events L M, Pr(L | M)<=1 *)
Lemma pr_cond_inf_1 : forall L M : Event V, (pr_cond L M <= 1)%R.
intros.
unfold pr_cond;unfold prob_cond in |- *.
unfold pr;unfold prob in |- *.
cut ({Pr M = 0} + {Pr M <> 0}).
intro.
case H.
intro.
rewrite inter_0 with (B := M).
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite Rmult_0_l.
auto with real.
auto.
intro.
assert
 ((INR (Pr (L //\ M)) / INR (lengthT E) /
   (INR (Pr M) / INR (lengthT E)))%R =
  (INR (Pr (L //\ M)) / INR (Pr M))%R).
apply div_simpl.
apply ax1.
unfold pr;unfold prob in |- *.
apply not_Req_0.
apply INR_length_E_not_0.
red in |- *; intro.
apply n.
apply INR_eq.
auto with real.
apply INR_length_E_not_0.
unfold Pr in H0;rewrite H0.
apply Rle_div_1.
apply ax5.
unfold pr;unfold prob in |- *.
apply not_Req_0.
apply INR_length_E_not_0.
red in |- *; intro.
apply n.
apply INR_eq.
auto with real.
apply le_INR.
apply le_inter_r.
apply Aeq_dec.
Qed.


(* for all events A B, Pr(A)<=Pr(B)+Pr(A | !B) *)
Lemma Rle_pr_pr_cond: forall A B : Event V,
 (pr A <=
  pr B + pr_cond A (! B))%R.
intros.
rewrite prob_eq_cond with (A:=A)(B:=B).
rewrite <-Rmult_1_l with (pr B).
rewrite <-Rmult_1_r with (pr_cond A (! B)).
rewrite Rmult_assoc.
apply Rle_Rmult_plus_distr;try apply pr_cond_sup0;
try rewrite Rmult_1_l; try apply prob_sup0 ;auto with * . 
apply pr_cond_inf_1.
apply inf_1.
Qed.


(* for all events A B C, 0<INR Pr(C) => Pr(A\\/B | C) <= Pr(A | C) +Pr(B | C) *)
Lemma pr_cond_union :
 forall A B C : Event V,
 (0 < INR (Pr C))%R ->
 (pr_cond (A \\/ B) C <= pr_cond A C + pr_cond B C)%R.
unfold pr_cond in |- *.
unfold prob_cond;unfold pr ;unfold prob.
intros.
rewrite Rdiv_Rdiv.
rewrite Rdiv_Rdiv.
rewrite Rdiv_Rdiv.
rewrite <- plus_Rplus_div.
apply Rle_div.
rewrite un_inter.
apply le_union.
auto.
apply not_0_Rlt_0; auto.
auto.
apply not_0_Rlt_0; auto.
auto.
apply not_0_Rlt_0; auto.
auto.
Qed.

(*for all events A B, Pr(A//\B)<=Pr(A | B) *)
Lemma Rle_inter_cond :
 forall A B : Event V, (pr (A //\ B) <= pr_cond A B)%R.
intros.
rewrite pr_cond_eq.
rewrite <- Rmult_1_r.
apply Rmult_le_compat.
unfold pr_cond;unfold prob_cond.
rewrite Rdiv_Rmult.
assert ({pr B = 0%R} + {pr B <> 0%R}).
apply Aeq_dec.
case H.
intros.
assert (pr (A //\ B) = 0%R).
unfold pr in |- *.
assert (Pr (A //\ B) = 0).
apply inter_0.
unfold pr in e;unfold prob in e.
rewrite Rdiv_Rmult in e.
assert (INR (Pr B) = 0%R \/ (/ INR (lengthT E))%R = 0%R).
apply Rmult_integral.
apply e.
assert ((/ INR (lengthT E))%R <> 0%R).
assert (0 < / INR (lengthT E))%R.
apply lgt_inv_E.
auto with *.
intuition.
unfold Pr in H0;unfold prob;rewrite H0.
rewrite Rdiv_Rmult.
auto with *.
unfold pr in H0;rewrite H0.
auto with *.
intros.
assert (pr B <= 1)%R.
apply inf_1.

assert (1 <= / pr B)%R.
rewrite <- Rinv_1.
apply Rle_Rinv.
assert (0 <= pr B)%R.
apply prob_ge_0.
assert ((0 < pr B)%R \/ (0 > pr B)%R).
apply Rdichotomy; auto with *.
assert (~ (pr B < 0)%R).
apply Rle_not_lt.
auto with *.
assert (~ (0 > pr B)%R).
auto with *.
intuition.
auto with *.
apply inf_1.
rewrite <- Rmult_1_r with (r := 0%R).
apply Rmult_le_compat.
auto with *.
auto with *.
apply prob_ge_0.
auto with *.
apply prob_sup0.
auto with *.
apply inf_1.
Qed.



(*----------------------- probabilities with list of events ---------------- *)

Definition EvIntL:=EvIntList V.
Definition EvDiffL:=EvDiffList V.
Definition EvUnL:=EvUnList V.

(*forall list of events M1,   ,Mn and x:V,
!M1/\   /\!Mn x <-> !(M1\/   \/Mn) x *)
Lemma eq_event_diff_list :
 forall (M : listT (Event V)) (x : V),
 EvIntL (EvDiffL M) x <-> ~ (EvUnL M) x.
simple induction M.
simpl in |- *.
intros; intuition.
simpl in |- *.
intros.
unfold iff in |- *.
split.
assert (~ a x /\ ~ EvUnL l x -> ~ (a x \/ EvUnL l x)).
intuition.
intros.
apply H0.
unfold iff in H.
assert (EvIntL (EvDiffL l) x -> ~ EvUnL l x).
elim (H x).
intuition.
split.
intuition.
apply H2; intuition.
intros.
split.
intuition.
unfold iff in H.
assert (~ EvUnL l x -> EvIntL (EvDiffL l) x).
elim (H x).
intuition.
apply H1.
intuition.
Qed.

(*pr (!M1/\   /\!Mn) <= pr(!(M1\/   \/Mn)) *)
Lemma prob_int_diff_list :
 forall M : listT (Event V),
 pr (EvIntL (EvDiffL M)) = pr (! (EvUnL M)).
intros.
assert
 (forall x : V, EvIntL (EvDiffL M) x <-> ~ (EvUnL M) x).
apply eq_event_diff_list.
apply prob_equiv.
auto with *.
Qed.


(*pr (M1\/   \/Mn) <= pr(M1) +   + pr(Mn) *)
Lemma prob_union_list :
 forall M : listT (Event V), (pr (EvUnL M) <= SumList (mapT pr M))%R.
intros.
induction  M as [| a M HrecM].
simpl in |- *.
unfold pr;unfold prob in |- *.
generalize evt_nul;unfold Pr;intro h;rewrite h.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
auto with *.
simpl in |- *.
apply Rle_trans with (r2 := (pr a + pr (EvUnL M))%R).
apply le_prob_un.
auto with *.
Qed.

(* pr (!M1/\   /\!Mn) = 1 - pr (M1\/  \/Mn) *)
Lemma ax9 :
 forall M : listT (Event V),
 pr  (EvIntL  (EvDiffL  M)) = (1 - pr (EvUnL  M))%R.
intros.
assert
 (pr  (EvIntL  (EvDiffL  M)) =
  pr  (!  (EvUnL  M))).
apply prob_int_diff_list.
rewrite H.
apply prob_diff_eq_min_1.
Qed.

(*forall list of events M1,   ,Mn and x:V,
 !(M1\/   \/Mn) x <=> !M1/\   /\!Mn x *)
Lemma DiffUnListdistr :
    forall (x : V) (M : listT (Event V)),
    (! (EvUnL  M)) x <-> EvIntL  (EvDiffL  M) x.
intros.
generalize (eq_event_diff_list M x);intro.
elim H;intros.
intuition.
Qed.

Definition pr_condL:=PrCondList V E.

(*
   Pr[M1]+...+Pr[Mn] < 1
           ->

                                    Pr[L]
   Pr[L|!M1 & ... & !Mn] <= -------------------------
                            1-(Pr[M1] + ... + Pr[Mn]) 
*)
Lemma PrCondList_sum :
 forall (L : Event V) (M : listT (Event V)),
 (SumList (mapT pr  M) < 1)%R ->
 (pr_condL L M <= pr  L / (1 - SumList (mapT pr  M)))%R.
intros.
apply
 RIneq.Rle_trans
  with (r2 := (pr L / pr (EvIntL (EvDiffL M)))%R).
unfold pr_condL in |- *.
unfold PrCondList;unfold pr;unfold pr_cond ;unfold prob_cond.
apply Rle_inv_monotony_r.
replace (prob V E (EvIntL (EvDiffL M))) with
 (pr (! (EvUnL M))).
assert
 (pr (! (EvUnL M)) = (1 - pr (EvUnL M))%R).
apply prob_diff_eq_min_1.
rewrite H0.
apply Rlt_minus_r.
apply RIneq.Rle_lt_trans with (r2 := SumList  (mapT pr M)).
apply prob_union_list.
apply H.
apply prob_equiv.
intros.
apply DiffUnListdistr.
apply prob_impl.
unfold EventInter in |- *.
simpl in |- *.
intuition.
apply Rle_inv_monotony.
apply Rlt_minus_r.
exact H.
assert
 (pr (EvIntL (EvDiffL M)) = (1 - pr (EvUnL M))%R).
apply ax9.
rewrite H0.
apply Rle_Ropp1_compatibility.
apply prob_union_list.
apply prob_ge_0.
Qed.
End Proofs.

(*---------------the probality space is an app-------------------------------*)
Section Pr_app.
Variable V:Type.
Variables E F:listT V.


(*Pr A in E@F = Pr A in E + Pr A in F *)
Lemma proba_app_eq:forall (A:Event V),Pr (E @ F) A=(Pr E A)+(Pr F A).
intros. 
unfold Pr;unfold Proba.
elim E.
elim F.
simpl;intros.
auto with * .
simpl;intros.
auto with * .
simpl;intros.
case (event_dec V A a).
simpl;intros.
auto with * .
simpl;intros.
auto with * .
Qed.


Lemma pr_app_eq:forall (A:Event V),
(pr (E @ F) A=INR (Pr  E A)/INR (lengthT (E @ F))+
INR (Pr F A)/INR (lengthT (E @ F)))%R.
intros. 
unfold pr;unfold prob.
rewrite proba_app_eq.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite plus_INR.
apply Rmult_plus_distr_r.
Qed.

Require Import Logic_Type.

Lemma Pr_listTp_eq_app:forall (W:Type)(g:listT W)(l:listT V)(a:V)(A:Event (prodT V W)),
Proba _ (listTprod (a :: l) g) A = 
Proba _ ((mapT (fun z:W=>pairT a z) g) @ (listTprod l g)) A.
unfold Proba;intros.
induction g.
simpl;intros;auto.
simpl;intros.
case (event_dec (prodT V W) A (pairT a a0)).
simpl;intros.
rewrite lgt_filt_app.
rewrite IHg.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
auto with * .
simpl;intros.
rewrite lgt_filt_app.
rewrite IHg.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
auto with * .
Qed.

Lemma pr_listTp_eq_app:forall (W:Type)(g:listT W)(l:listT V)(a:V)(A:Event (prodT V W)),
prob _ (listTprod (a :: l) g) A = 
prob _ ((mapT (fun z:W=>pairT a z) g) @ (listTprod l g)) A.
intros.
unfold prob.
rewrite Pr_listTp_eq_app.
rewrite lgt_listp_cons_eq.
auto with * .
Qed.
End Pr_app.

(*-----------------Event of type V to Event of type VxW----------------------*)

Section Pr_listp.
Variables V W:Type.
Variable Ev:listT V.
Variable Ew:listT W.
Hypothesis length_Ev_not_0 : lengthT Ev <> 0.
Hypothesis length_Ew_not_0 : lengthT Ew <> 0.

Definition mk_evF:=mk_ev_fst V W.
Definition mk_evS:=mk_ev_snd V W.

(* Pr A in EvxEw = #Ew * Pr A in Ev *)
Lemma eq_pr_mkfst:forall A : Event V,(Pr (listTprod Ev Ew)
         (mk_evF A))=(lengthT Ew)*(Pr Ev A).
unfold Pr;unfold Proba.
elim Ev.
elim Ew.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim Ew.
simpl;intros;auto.
simpl;intros a0 l0.
case ( dec_pred_fst V W A (ev_dec V A) (pairT a a0)).
case ( event_dec V A a).
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
unfold mk_evF;rewrite eq_mkfst_map.
auto with *.
simpl;intros;intuition.
simpl;intro.
case ( event_dec V A a).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
unfold mk_evF;rewrite eq_mkfst_map.
auto with *.
Qed.

(* pr A in Ev = pr A in EvxEw *)
Lemma  prod_mk_ev_fst :
    forall A : Event V,
    pr Ev A = pr (listTprod Ev Ew) (mk_evF A).
unfold pr;unfold prob.
intros.
rewrite lgt_listp.
rewrite eq_pr_mkfst.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_comm with (r1:=(INR (lengthT Ew))).
rewrite RIneq.Rinv_mult_distr.
rewrite Rmult_comm with (r1:=(Rinv (INR (lengthT Ev)))).
rewrite<- Rmult_assoc.
unfold Pr.
replace (INR (Proba _ Ev A) * INR (lengthT Ew) * / INR (lengthT Ew) *
    / INR (lengthT Ev))%R with (INR (Proba _ Ev A) * (INR (lengthT Ew) * / INR (lengthT Ew) )*
    / INR (lengthT Ev))%R.
rewrite Rmult_comm with (r1:=(INR (lengthT Ew))).
rewrite <-RIneq.Rinv_l_sym with (r:=INR (lengthT Ew)).
replace  (INR (Proba _ Ev A) * 1 * / INR (lengthT Ev))%R with 
(INR (Proba _ Ev A) * (1 * / INR (lengthT Ev)))%R.
rewrite Rmult_1_l.
auto with *.
auto with *.
apply INR_length_E_not_0;auto.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
auto with *.
apply INR_length_E_not_0;auto.
apply INR_length_E_not_0;auto.
Qed.

(* A a-> Pr A in {(z,l), z in l}=# l *)
Lemma eq_snd: forall (A : Event W) (a:W)(l:listT V),
(A a)->
Pr (mapT (fun z : V => pairT z a) l) (mk_evS A)=(lengthT l).
unfold Pr;unfold Proba.
induction l.
simpl;intros;auto.
simpl;intros.
case ( dec_pred_snd  V W A (ev_dec W A) (pairT a0 a)).
simpl;intros.
auto with *.
simpl;intros;intuition.
Qed.

(* ~A a-> Pr A in {(z,l), z in l}=0 *)
Lemma not_eq_snd: forall (A : Event W) (a:W)(l:listT V),~(A a)->
Pr (mapT (fun z : V => pairT z a) l) (mk_evS A)=0.
unfold Pr;unfold Proba.
induction l.
simpl;intros;auto.
simpl;intros.
case ( dec_pred_snd  V W A (ev_dec W A) (pairT a0 a)).
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.

(*Pr A in EvxEw = # Ev * Pr A in Ew *)
Lemma eq_pr_mksnd:forall A : Event W,(Pr (listTprod Ev Ew)
         (mk_evS A))=(lengthT Ev)*(Pr Ew A).
unfold Pr;unfold Proba.
elim Ev.
elim Ew.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim Ew.
simpl;intros;auto.
simpl;intros a0 l0.
case (  dec_pred_snd V W A (ev_dec W A) (pairT a a0)).
case (event_dec W A a0 ).
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
generalize eq_snd;unfold Pr;unfold Proba;
intro heq;rewrite heq.
apply eq_S_simpl .
auto.
simpl;intros;intuition.
case (event_dec W A a0).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
generalize not_eq_snd;unfold Pr;
unfold Proba;intro h;rewrite h.
auto.
auto.
Qed.

(*pr A in Ew = pr A in EvxEw   *)
Lemma prod_mk_ev_snd: forall A : Event W,
    pr  Ew  A =pr (listTprod Ev Ew) (mk_evS A).
unfold pr;unfold prob.
intros.
rewrite lgt_listp.
rewrite eq_pr_mksnd.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_comm with (r1:=(INR (lengthT Ev))).
rewrite RIneq.Rinv_mult_distr.
rewrite<- Rmult_assoc.
replace  (INR (Pr Ew A) * INR (lengthT Ev) * / INR (lengthT Ev) * / INR (lengthT Ew))%R
 with (INR (Proba _ Ew A) *( INR (lengthT Ev) * / INR (lengthT Ev)) *
    / INR (lengthT Ew))%R .
rewrite Rmult_comm with (r1:=(INR (lengthT Ev))).
rewrite <-RIneq.Rinv_l_sym with (r:=INR (lengthT Ev)).
replace  (INR (Proba _ Ew A) * 1 * / INR (lengthT Ew))%R with 
(INR (Proba _ Ew  A) * (1 * / INR (lengthT Ew)))%R.
rewrite Rmult_1_l.
auto with *.
auto with *.
auto with *.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
auto with *.
auto with *.
auto with *.
Qed.
End Pr_listp.

Section pr_pdT.
Variables V :Type.
Variable Ev:listT V.
Hypothesis length_Ev_not_0 : lengthT Ev <> 0.

 Notation "x //\ y" := (EventInter (prodT V V) x y).
 Notation "x \\/ y" := (EventUnion (prodT V V) x y).
 Notation " ! x " := (Eventdiff (prodT V V) x).

(*A a-> Pr (A /\ B) in {(a,z), z in l} = Pr B in l *)
Lemma lgt_filt_inter :
 forall (l : listT V) (A B : Event V) (a : V),
 A a ->
Pr (mapT (fun z : V => pairT a z) l) ((mk_evF V A) //\ (mk_evS V B))
 = Pr l B.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros; auto.
simpl in |- *; intros.
case
 (event_inter_aux (prodT V V) (mk_evF V A) (mk_evS V B)
    (pairT a0 a)).
case (event_dec V B a).
simpl in |- *; intros.
apply eq_S.
apply H; auto.
simpl in |- *; intros.
intuition.
case (event_dec V B a).
simpl in |- *; intros.
intuition.
intros; apply H; auto.
Qed.

(*~A a-> Pr (A /\ B) in {(a,z), z in l} = 0 *)
Lemma lgt_filt_inter_not :
 forall (l : listT V) (A B : Event V) (a : V),
 ~ A a ->
Pr (mapT (fun z : V => pairT a z) l)
 ((mk_evF V A) //\ (mk_evS V B)) = 0.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros; auto.
simpl in |- *; intros.
case
 (event_inter_aux (prodT V V) (mk_evF V A) (mk_evS V B)
    (pairT a0 a)).
case (event_dec V B a).
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
apply H; auto.
Qed.

(* Pr A in {(z,a) z in l} = Pr A in l *)
Lemma eq_fst_map:forall (A:Event V) (a:V)(l:(listT V)),
Pr (mapT (fun z : V => pairT z a) l) (mk_evF V A)
= (lengthT (filt A l)).
unfold Pr;unfold Proba.
induction l.
simpl;intros;auto.
simpl;intros.
case (dec_pred_fst V V A (ev_dec V  A) (pairT a0 a)).
case (event_dec V A a0).
simpl;intros.
auto with *.
simpl;intros;intuition.
case (event_dec V A a0).
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.


(* Pr A in lxg = #g * Pr A in l *)
Lemma eq_pr_mkfst_:forall (l g:listT V)(A : Event V),(Pr (listTprod l g)
         (mk_evF V A))=(lengthT g)*(Pr l A).
intros;unfold Pr;unfold Proba.
elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim g.
simpl;intros;auto.
simpl;intros a0 l1.
case ( dec_pred_fst V V A (ev_dec V A) (pairT a a0)).
case ( event_dec V A a).
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
generalize eq_fst_map;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with *.
simpl;intros;intuition.
simpl;intro.
case ( event_dec V A a).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
generalize eq_fst_map;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with *.
Qed.

(* A a-> Pr A in {(a,z), z in l} = #l *)
Lemma lgt_filt_map :
 forall (l : listT V) (A : Event V) (a : V),
 A a ->
Pr (mapT (fun z : V => pairT a z) l) (mk_evF V A) =
 lengthT l.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (dec_pred_fst V V A (ev_dec V  A) (pairT a0 a)).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
intuition.
Qed.

(* ~A a-> Pr A in {(a,z), z in l} = 0 *)
Lemma lgt_filt_map_not :
 forall (l : listT V) (A : Event V) (a : V),
 ~ A a ->
Pr (mapT (fun z : V => pairT a z) l) (mk_evF V A) = 0.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (dec_pred_fst V V A (ev_dec V A) (pairT a0 a)).
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
intuition.
Qed.

(* ~A a-> Pr A in {(z,a), z in l} = 0 *)
Lemma lgt_filt_map_not_l :
 forall (l : listT V) (A : Event V) (a : V),
 ~ A a ->
Pr (mapT (fun z : V => pairT z a) l) (mk_evS V A) = 0.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (dec_pred_snd V V A (ev_dec V A) (pairT a a0)).
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
intuition.
Qed.

(*A a-> Pr A in {(z,a), z in l} = #l *)
Lemma lgt_filt_map_l :
 forall (l : listT V) (A : Event V) (a : V),
 A a ->
Pr (mapT (fun z : V => pairT z a) l) (mk_evS V A) =
 lengthT l.
unfold Pr;unfold Proba.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (dec_pred_snd V V A (ev_dec V A) (pairT a a0)).
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
intuition.
Qed.

(*Pr B in l2 * #l1 = Pr B in l1*l2 *)
Lemma lgt_filt_mksd :
 forall (l2 l1 : listT V) (B : Event V),
Pr l2 B  * lengthT l1 =
Pr (listTprod l1 l2) (mk_evS V B) .
unfold Pr;unfold Proba.
intros.
induction  l2 as [| a l2 Hrecl2].
induction  l1 as [| a l1 Hrecl1].
simpl in |- *.
auto.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec V B a).
simpl in |- *.
rewrite lgt_filt_app.
simpl in |- *; intros.
generalize lgt_filt_map_l;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with *.
auto.
simpl in |- *; intros.
generalize lgt_filt_app;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite Hrecl2.
generalize lgt_filt_map_not_l;unfold Pr;
unfold Proba;intro h;rewrite h.
auto with *.
auto.
Qed.

End pr_pdT.


(*----------------------Event of type V to Event of type WxWxV---------------*)

Section pr_PdT.
Variables V W:Type.
Variable Ev:listT V.
Variable Ew:listT W.
Hypothesis length_Ev_not_0 : lengthT Ev <> 0.
Hypothesis length_Ew_not_0 : lengthT Ew <> 0.

Definition mk_ev_F:=mk_pdT_ev_fst (V:=V) W.
Definition mk_ev_S:=mk_pdT_ev_snd (V:=V) W.
Definition mk_ev_T:=mk_pdT_ev_trd W.

 Notation "x //\ y" := (EventInter _ x y).
 Notation "x \\/ y" := (EventUnion _ x y).
 Notation " ! x " := (Eventdiff _  x).

(*A a-> Pr A in {(z,a0,a), z in l} = # l *)
Lemma lgt_filt_mk:forall (A:Event V)(l:listT W)(a:V)(a0:W),
A a->
Pr (mapT (fun z : W => tripleT z a0 a) l) (mk_ev_T A)
=(lengthT l).
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_trd (ev_dec V A) (tripleT a a1 a0)).
simpl;intros.
case (dec_eq_nat (lengthT l) 0).
intro heq;rewrite heq.
rewrite (lgt_0_eq_nil heq);simpl;auto.
intro;auto with * . 
simpl;intro;intuition.
Qed.

(*A a-> Pr A in {(a0,z,a), z in l} = # l *)
Lemma lgt_filt_mk_snd:forall (A:Event V)(a0:W)(a1:V)(l:listT W),
A a1->
Pr (mapT (fun z : W => tripleT a0 z a1) l) (mk_ev_T A)
=lengthT l.
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_trd  (ev_dec V A) (tripleT a0 a a1)).
simpl;intros.
auto with * . 
simpl;intro;intuition.
Qed.

(*~A a-> Pr A in {(a0,z,a), z in l} = 0 *)
Lemma lgt_filt_mk_snd_not:forall (A:Event V)(a0:W)(a1:V)(l:listT W),
~(A a1)->
Pr (mapT (fun z : W => tripleT a0 z a1) l) (mk_ev_T A)=0.
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_trd (ev_dec V A) (tripleT a0 a a1)).
simpl;intro;intuition.
simpl;intros.
auto with * . 
Qed.

(*A a0-> Pr A in {(a0,z,a), z in l} = # l *)
Lemma lgt_filt_mk_fst:forall (A : Event V)(a0:V)(a1:W)(l:listT V),
(A a0)->
Pr (mapT (fun z : V=> tripleT a0 z a1) l) (mk_ev_F A)=lengthT l.
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_fst (ev_dec V A) (tripleT a0 a a1)).
simpl;intros.
auto with * . 
simpl;intro;intuition.
Qed.

(*~A a0-> Pr A in {(a0,z,a), z in l} = 0 *)
Lemma lgt_filt_mk_fst_not:forall (A : Event V)(a0:V)(a1:W)(l:listT V),
~(A a0)->
Pr (mapT (fun z : V => tripleT a0 z a1) l) (mk_ev_F A)=0.
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_fst (ev_dec V A) (tripleT a0 a a1)).
simpl;intro;intuition.
simpl;intros.
auto with * . 
Qed.

(* Pr A in {(a0,z,a1), z in l} = Pr A in l *)
Lemma lgt_filt_mk_snd_:forall (A : Event V)(a0:V)(a1:W)(l:listT V),
Pr (mapT (fun z : V => tripleT a0 z a1) l) (mk_ev_S A)
=Pr l A.
unfold Pr;unfold Proba.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_lem_snd (ev_dec V A) (tripleT a0 a a1)).
case (event_dec V A a).
simpl;intros.
auto with * . 
simpl;intros.
intuition.
case (event_dec V A a).
simpl;intros.
intuition. 
simpl;intros.
auto with * .
Qed.

(* Pr A in axhxg = #h * Pr A in g *)
Lemma lgt_list_fst_fix_eq:forall (g:listT V)(h:listT W)(A : Event V)(a:W),
Pr (listPd_fst_fix a h g) (mk_ev_T A)=(lengthT h)*(Pr g A).
unfold Pr;unfold Proba.
intros;elim h.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim g.
simpl;intros;auto.
simpl;intros.
case (dec_pdT_lem_trd (ev_dec V A) (tripleT a a0 a1)).
case (event_dec V A a1).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
generalize lgt_filt_mk_snd;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.eq_mult_S.
auto with * .
auto.
simpl;intros;intuition.
case (event_dec V A a1).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
generalize lgt_filt_mk_snd_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with * .
auto.
Qed.

(* A a->Pr A in axhxg = #l * #g *)
Lemma lgt_fst_fix_eq: forall (g:listT W)(l:listT V)(A : Event V)(a:V),
A a->
Pr (listPd_fst_fix a l g) (mk_ev_F A)=(lengthT l)*(lengthT g).
unfold Pr;unfold Proba.
intros;elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim g.
simpl;intros;auto.
simpl;intros.
case (dec_pdT_lem_fst (ev_dec V A) (tripleT a a0 a1)).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H1;rewrite H1.
generalize lgt_filt_mk_fst;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.eq_mult_S.
auto with * .
auto.
simpl;intros.
intuition.
Qed.

(* ~A a->Pr A in axhxg = 0 *)
Lemma lgt_fst_fix_eq_not: forall (g:listT W)(l:listT V)(A : Event V)(a:V),
~ A a->
Pr (listPd_fst_fix a l g) (mk_ev_F A)=0.
unfold Pr;unfold Proba.
intros;elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim g.
simpl;intros;auto.
simpl;intros.
case (dec_pdT_lem_fst (ev_dec V A) (tripleT a a0 a1)).
simpl;intros.
intuition.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H1;rewrite H1.
generalize lgt_filt_mk_fst_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto.
auto.
Qed.

(*Pr A in axlxg = #g * Pr A in l *)
Lemma lgt_list_snd_fix_eq:forall (g:listT W)(l:listT V)(A : Event V)(a:V),
Pr (listPd_fst_fix a l g) (mk_ev_S A)=(lengthT g)* Pr l A.
unfold Pr;unfold Proba.
intros;elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim g.
simpl;intros;auto.
simpl;intros a1 l1.
case (dec_pdT_lem_snd (ev_dec V A) (tripleT a a0 a1)).
case (event_dec V A a0).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
generalize lgt_filt_mk_snd_;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with * .
simpl;intros;intuition.
case (event_dec V A a0).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
generalize lgt_filt_mk_snd_;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with * .
Qed.

(*Pr A in hxlxg = #h * #g * Pr A in g *)
Lemma eq_pr_mktrd:forall (g:listT V)(l h:listT W)(A : Event V),(Pr (listPd h l g )
         (mk_ev_T A))=(lengthT h)*(lengthT l)*(Pr g A).
unfold Pr;unfold Proba.
intros;elim h.
elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
generalize lgt_list_fst_fix_eq;unfold Pr;
unfold Proba;intro heq;rewrite heq.
unfold Pr;unfold Proba.
rewrite H.
auto with * .
Qed.

(*Pr A in hxlxg = #l * #g * Pr A in h *)
Lemma eq_pr_mkfst_pdT:forall (g:listT W)(h l:listT V)(A : Event V),
(Pr (listPd h l g )
         (mk_ev_F A))=(lengthT l)*(lengthT g)*(Pr h A).
unfold Pr;unfold Proba.
intros;elim h.
elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
case (event_dec V A a).
simpl;intro.
rewrite H.
generalize lgt_fst_fix_eq;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.mult_S.
auto with * .
auto.
simpl;intros.
rewrite H.
generalize lgt_fst_fix_eq_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto.
auto.
Qed.

(*Pr A in hxlxg = #h * #g * Pr A in l *)
Lemma eq_pr_mksnd_:forall (g:listT W)(h l:listT V)(A : Event V),
(Pr (listPd h l g)
         (mk_ev_S A))=(lengthT h)*(lengthT g)*(Pr l A).
unfold Pr;unfold Proba.
intros;elim h.
elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.
generalize lgt_list_snd_fix_eq;unfold Pr;
unfold Proba;intro heq;rewrite heq.
auto with * .
Qed.

(* A a->B a0-> Pr A/\B in {(a,a0,z)::(a,y,z) y in l0 z in l}=
#l + Pr A/\B in {(a,y,z) y in l0 z in l} *)
Lemma lgt_list_fix_cons:forall (A B: Event V)(a a0:V)(l:listT W)(l0:listT V),
A a->B a0->
Pr (listPd_fst_fix a (a0 :: l0) l) ((mk_ev_F A) //\ (mk_ev_S B))
= lengthT l + Pr (listPd_fst_fix a l0 l) ((mk_ev_F A) //\ (mk_ev_S B)).
unfold Pr;unfold Proba. 
intros;elim l.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux _
           (mk_ev_F A) (mk_ev_S B)
           (tripleT a a0 a1)).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H1;rewrite H1.
rewrite lgt_filt_app.
auto with * . 
auto.
auto.
simpl;intros;intuition.
Qed.

(* ~A a->~B a0-> Pr !A/\!B in {(a,a0,z)::(a,y,z) y in l0 z in l}=
#l + Pr !A/\!B in {(a,y,z) y in l0 z in l} *)
Lemma lgt_list_fix_cons_diff:forall (A B: Event V)(a a0:V)(l:listT W)(l0:listT V),
~A a->~B a0->
Pr (listPd_fst_fix a (a0 :: l0) l) ((! (mk_ev_F A)) //\ (! (mk_ev_S B)))
= lengthT l +Pr (listPd_fst_fix a l0 l) ((! (mk_ev_F A)) //\ (! (mk_ev_S B))).
unfold Pr;unfold Proba. 
intros;elim l.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux _ (!(mk_ev_F A)) (!(mk_ev_S B)) (tripleT a a0 a1)).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H1;rewrite H1.
rewrite lgt_filt_app.
auto with * . 
auto.
auto.
simpl;intros.
intuition.
Qed.

(* ~(A a/\B a0)-> Pr A/\B in {(a,a0,z)::(a,y,z) y in l0 z in l}=
 Pr A/\B in {(a,y,z) y in l0 z in l} *)
Lemma lgt_list_fix_cons_not:forall (A B: Event V)(a a0:V)(l:listT W)(l0:listT V),
~(A a/\B a0)->
Pr (listPd_fst_fix a (a0 :: l0) l) ((mk_ev_F A) //\ (mk_ev_S B))
=Pr (listPd_fst_fix a l0 l) ((mk_ev_F A) //\ (mk_ev_S B)).
unfold Pr;unfold Proba.
intros;elim l.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux _
           (mk_ev_F A) (mk_ev_S B)
           (tripleT a a0 a1)).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_filt_app.
auto with * . 
Qed.

(* ~(~A a/\~B a0)-> Pr !A/\!B in {(a,a0,z)::(a,y,z) y in l0 z in l}=
 Pr !A/\!B in {(a,y,z) y in l0 z in l} *)
Lemma lgt_list_fix_cons_diff_not:forall (A B: Event V)(a a0:V)(h:listT W)(l0:listT V),
~(~A a/\~B a0)->
Pr (listPd_fst_fix a (a0 :: l0) h) ((! (mk_ev_F A)) //\ (! (mk_ev_S B)))
=Pr (listPd_fst_fix a l0 h) ((! (mk_ev_F A)) //\ (! (mk_ev_S B))).
unfold Pr;unfold Proba. 
intros;elim h.
simpl;intros;auto.
simpl;intros.
case (event_inter_aux _ (!(mk_ev_F A))
           (!(mk_ev_S B)) (tripleT a a0 a1)).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_filt_app.
auto with * . 
Qed.

(* Pr A/\B in lxgxh= #h * Pr A/\B in l*g *)
Lemma eq_pr_mk_fst_snd:forall (A B: Event V)(h:listT W)(l g:listT V),
Pr (listPd l g h) ((mk_ev_F A) //\ (mk_ev_S B))=
lengthT h * Pr (listTprod l g) ((mk_evF V A)//\ (mk_evS V B)).
unfold Pr;unfold Proba;intros.
elim l.
elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.


elim g.
simpl;intros.
rewrite list_fix_nil;simpl;auto.
simpl;intros.
case (event_inter_aux _
           (mk_evF V A) (mk_evS V B) (pairT a a0)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.eq_mult_S.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt.
auto with * . 
intuition.
intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt;auto with * . 
auto.
Qed.

(*Pr !A/\!B in lxgxh = #h * Pr !A/\!B in l*g *)
Lemma eq_pr_mk_fst_snd_diff:forall (A B: Event V)(h:listT W)(l g:listT V),
Pr (listPd l g h) ((! (mk_ev_F A)) //\ (! (mk_ev_S B)))=lengthT h * Pr (listTprod l g) 
((! (mk_evF V A)) //\ (! (mk_evS V B))).
unfold Pr;unfold Proba.
intros;elim l.
elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.

elim g.
simpl;intros.
rewrite list_fix_nil;simpl;auto.
simpl;intros.
case (event_inter_aux _
           (! (mk_evF V A))
           (! (mk_evS V B))
           (pairT a a0)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons_diff;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.eq_mult_S.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt;auto with * . 
intuition.
intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons_diff_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt;auto with * . 
auto.
Qed.

(*pr A in h = pr A in lxgxh *)
Lemma  prod_mk_pdT_ev_trd :
    forall (A : Event V)(l g:listT W)(h:listT V),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
    pr h A = pr (listPd l g h) (mk_ev_T A).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT_.
rewrite eq_pr_mktrd.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rmult_comm with (r2:=(INR (lengthT h))). 
rewrite Rdiv_Rmult_simpl_.
auto.
generalize (Rmult_eq_0  (INR (lengthT l)) ( INR (lengthT g))).
intros;intuition.
auto with * .
Qed.

(*pr A in l = pr A in lxgxh *)
Lemma  prod_mk_pdT_ev_fst :
    forall (A : Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
    pr l A = pr (listPd l g h) (mk_ev_F A).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT_.
rewrite eq_pr_mkfst_pdT.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1:=(INR (lengthT l))%R). 
rewrite <-Rmult_assoc.
rewrite Rmult_comm with (r2:=(INR (lengthT l))%R). 
rewrite Rdiv_Rmult_simpl_.
auto.
generalize (Rmult_eq_0  (INR (lengthT g)) ( INR (lengthT h))).
intros;intuition.
auto with * .
Qed.

(*pr A in g = pr A in lxgxh *)
Lemma  prod_mk_pdT_ev_snd :
    forall (A : Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
    pr g A = pr (listPd l g h) (mk_ev_S A).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT_.
rewrite eq_pr_mksnd_.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rmult_assoc.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1:=(INR (lengthT g))%R). 
rewrite <-Rmult_assoc.
rewrite <-Rmult_assoc.
rewrite Rmult_comm with (r2:=(INR (lengthT g))%R). 
rewrite Rdiv_Rmult_simpl_.
auto.
generalize (Rmult_eq_0  (INR (lengthT l)) ( INR (lengthT h))).
intros;intuition.
auto with * .
Qed.

(* pr A/\B in lxgxh = pr A/\B in l*g *)
Lemma prod_mk_pdT_ev_inter :
    forall (A B: Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
pr (listPd l g h) 
     ((mk_ev_F A) //\ (mk_ev_S B))=
       pr (listTprod l g) ((mk_evF V A) //\ (mk_evS V B)).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT.
rewrite <-listTprod_lengthT_.
rewrite eq_pr_mk_fst_snd.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rdiv_Rmult_simpl_.
auto with * .
auto with * .
generalize (Rmult_eq_0  (INR (lengthT l)) ( INR (lengthT g))).
intros;intuition. 
Qed.

(* pr !A/\!B in lxgxh = pr !A/\!B in l*g *)
Lemma prod_mk_pdT_ev_inter_diff : forall (A B: Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
pr (listPd l g h) 
     ((! (mk_ev_F A)) //\ (! (mk_ev_S B)))=
  pr (listTprod l g) ((! (mk_evF V A)) //\ (! (mk_evS V B))).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT.
rewrite <-listTprod_lengthT_.
rewrite eq_pr_mk_fst_snd_diff.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rdiv_Rmult_simpl_.
auto with * .
auto with * .
generalize (Rmult_eq_0  (INR (lengthT l)) ( INR (lengthT g))).
intros;intuition. 
Qed.

(* Pr A/\B in lxgxh = #h * Pr A/\B in l*g *)
Lemma eq_pr_mk_fst_snd_pdT:forall (A B: Event V)(l g:listT V)(h:listT W),
Pr (listPd l g h) ((mk_ev_F A) //\ (mk_ev_S B))=
lengthT h * Pr (listTprod l g) ((mk_evF V A) //\ (mk_evS V B)).
unfold Pr;unfold Proba.
intros;elim l.
elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.


elim g.
simpl;intros.
rewrite list_fix_nil;simpl;auto.
simpl;intros.
case (event_inter_aux _
           (mk_evF V A) (mk_evS V B) (pairT a a0)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite N_lemma.eq_mult_S.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt;auto with * . 
intuition.
intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
generalize lgt_list_fix_cons_not;unfold Pr;
unfold Proba;intro heq;rewrite heq.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
unfold filt;auto with * . 
auto.
Qed.


Lemma  prod_mk_prod_ev_fst_diff :
    forall (A : Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
pr l (! A) =
pr (listPd l g h) (!(mk_ev_F A)).
intros.
rewrite prob_diff_eq_min_1.
rewrite (prod_mk_pdT_ev_fst A H H0 H1).
rewrite prob_diff_eq_min_1.
auto with *.
apply lgt_listp_not_eq;auto.
auto.
Qed.


Lemma  prod_mk_prod_ev_snd_diff :
    forall (A : Event V)(l g:listT V)(h:listT W),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
pr g (! A) =
pr (listPd l g h)(!(mk_ev_S A)).
intros.
rewrite prob_diff_eq_min_1.
rewrite (prod_mk_pdT_ev_snd A H H0 H1).
rewrite prob_diff_eq_min_1.
auto with *.
apply lgt_listp_not_eq;auto.
auto.
Qed.


Lemma lgt_map_diff_eq:forall (A:Event V)(a0:V)(a1:W)(l:listT V),(lengthT
        (filt (!(mk_ev_F A))
           (mapT (fun z : V => tripleT a0 z a1) l)))=
 (lengthT
        (filt (mk_ev_F (! A))
           (mapT (fun z : V => tripleT a0 z a1) l))).
induction l;simpl;intros;auto.
case (event_diff_aux _
           (mk_ev_F A) (tripleT a0 a a1)).
simpl;intro.
change (S (lengthT (filt (!mk_ev_F A) (mapT (fun z : V => tripleT a0 z a1) l))) =
   lengthT
     (if dec_pdT_lem_fst (ev_dec V (Eventdiff V A)) (tripleT a0 a a1)
      then
        (tripleT a0 a a1) ::
         (filt (mk_ev_F (Eventdiff V A))
            (mapT (fun z : V => tripleT a0 z a1) l))
      else
       filt (mk_ev_F (Eventdiff V A)) (mapT (fun z : V => tripleT a0 z a1) l))).
case (dec_pdT_lem_fst (ev_dec V (Eventdiff _ A))
           (tripleT a0 a a1)).
simpl;intros.
auto.
simpl;intros;intuition.
simpl;intro.
change (lengthT (filt (!mk_ev_F A) (mapT (fun z : V => tripleT a0 z a1) l)) =
   lengthT
     (if dec_pdT_lem_fst (ev_dec V (Eventdiff V A)) (tripleT a0 a a1)
      then
       (tripleT a0 a a1) ::
         (filt (mk_ev_F (Eventdiff V A))
            (mapT (fun z : V => tripleT a0 z a1) l))
      else
       filt (mk_ev_F (Eventdiff V A)) (mapT (fun z : V => tripleT a0 z a1) l))).
case (dec_pdT_lem_fst (ev_dec V (Eventdiff _ A))
           (tripleT a0 a a1)).
simpl;intros;intuition.
simpl;intros;auto.
Qed.

Lemma lgt_map_diff_eq_snd:forall (A:Event V)(a0:V)(a1:W)(l:listT V),(lengthT
        (filt (!(mk_ev_S A))
           (mapT (fun z : V => tripleT a0 z a1) l)))=
 (lengthT
        (filt (mk_ev_S (! A))
           (mapT (fun z : V => tripleT a0 z a1) l))).
induction l;simpl;intros;auto.
case (event_diff_aux _
           (mk_ev_S A) (tripleT a0 a a1)).
simpl;intro.
change (S (lengthT (filt (!mk_ev_S A) (mapT (fun z : V => tripleT a0 z a1) l))) =
   lengthT
     (if dec_pdT_lem_snd (ev_dec V (!A)) (tripleT a0 a a1)
      then
        (tripleT a0 a a1) ::
         (filt (mk_ev_S (!A)) (mapT (fun z : V => tripleT a0 z a1) l))
      else filt (mk_ev_S (!A)) (mapT (fun z : V => tripleT a0 z a1) l))).
case (dec_pdT_lem_snd (ev_dec V (!A)) (tripleT a0 a a1)).
simpl;intros.
auto.
simpl;intros;intuition.
simpl;intro.
change (lengthT (filt (!mk_ev_S A) (mapT (fun z : V => tripleT a0 z a1) l)) =
   lengthT
     (if dec_pdT_lem_snd (ev_dec V (!A)) (tripleT a0 a a1)
      then
        (tripleT a0 a a1) ::
         (filt (mk_ev_S (!A)) (mapT (fun z : V => tripleT a0 z a1) l))
      else filt (mk_ev_S (!A)) (mapT (fun z : V => tripleT a0 z a1) l))).
case (dec_pdT_lem_snd (ev_dec V (! A))
           (tripleT a0 a a1)).
simpl;intros;intuition.
simpl;intros;auto.
Qed.


Lemma lgt_diff_mk_eq_mk_diff:forall (A:Event V)(a:V)(g:listT V)(h:listT W),lengthT
     (filt (!(mk_ev_F A)) (listPd_fst_fix a g h))=
lengthT
     (filt (mk_ev_F (! A))
        (listPd_fst_fix a g h)).
intros;elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim h.
simpl;intros;auto.
simpl;intros.
case (event_diff_aux _
           (mk_ev_F A) (tripleT a a0 a1)).
intro.
change (lengthT
     ( (tripleT a a0 a1) ::
        (filt (!mk_ev_F A)
           ((mapT (fun z : V => tripleT a z a1) l) @
              (listPd_fst_fix a (a0 :: l) l0)))) =
   lengthT
     (if dec_pdT_lem_fst (ev_dec V (!A)) (tripleT a a0 a1)
      then
       (tripleT a a0 a1) ::
         (filt (mk_ev_F (!A))
            ((mapT (fun z : V => tripleT a z a1) l) @
               (listPd_fst_fix a (a0 :: l) l0)))
      else
       filt (mk_ev_F (!A))
         ((mapT (fun z : V => tripleT a z a1) l) @
            (listPd_fst_fix a (a0 :: l) l0))) ).
case (dec_pdT_lem_fst (ev_dec V (! A))
           (tripleT a a0 a1)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_map_diff_eq.
auto with * .
simpl;intros;intuition.
simpl;intros.
change (lengthT
     (filt (!mk_ev_F A)
        ((mapT (fun z : V => tripleT a z a1) l) @
           (listPd_fst_fix a (a0 :: l) l0))) =
   lengthT
     (if dec_pdT_lem_fst (ev_dec V (!A)) (tripleT a a0 a1)
      then
       (tripleT a a0 a1) ::
         (filt (mk_ev_F (!A))
            ((mapT (fun z : V => tripleT a z a1) l) @
               (listPd_fst_fix a (a0 :: l) l0)))
      else
       filt (mk_ev_F (!A))
         ((mapT (fun z : V => tripleT a z a1) l) @
            (listPd_fst_fix a (a0 :: l) l0))) ).
case (dec_pdT_lem_fst (ev_dec V (! A))
           (tripleT a a0 a1)).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_map_diff_eq.
auto with * .
Qed.


Lemma lgt_diff_mk_eq_mk_diff_snd:
forall (A:Event V)(a:V)(g:listT V)(h:listT W),
lengthT
     (filt (!(mk_ev_S A)) (listPd_fst_fix a g h))=
lengthT
     (filt (mk_ev_S (! A))
        (listPd_fst_fix a g h)).
intros;elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim h.
simpl;intros;auto.
simpl;intros.
case (event_diff_aux _
           (mk_ev_S A) (tripleT a a0 a1)).
intro.
change (lengthT
     ((tripleT a a0 a1) ::
        (filt (!mk_ev_S A)
           ((mapT (fun z : V => tripleT a z a1) l) @
              (listPd_fst_fix a (a0 :: l) l0)))) =
   lengthT
     (if dec_pdT_lem_snd (ev_dec V (!A)) (tripleT a a0 a1)
      then
       (tripleT a a0 a1) ::
         (filt (mk_ev_S (!A))
            ((mapT (fun z : V => tripleT a z a1) l) @
               (listPd_fst_fix a (a0 :: l) l0)))
      else
       filt (mk_ev_S (!A))
         ((mapT (fun z : V => tripleT a z a1) l) @
            (listPd_fst_fix a (a0 :: l) l0)))).
case (dec_pdT_lem_snd (ev_dec V (! A))
           (tripleT a a0  a1)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_map_diff_eq_snd.
auto with * .
simpl;intros;intuition.
simpl;intros.
change (lengthT
     (filt (!mk_ev_S A)
        ((mapT (fun z : V => tripleT a z a1) l) @
           (listPd_fst_fix a (a0 :: l) l0))) =
   lengthT
     (if dec_pdT_lem_snd (ev_dec V (!A)) (tripleT a a0 a1)
      then
       (tripleT a a0 a1) ::
         (filt (mk_ev_S (!A))
            ((mapT (fun z : V => tripleT a z a1) l) @
               (listPd_fst_fix a (a0 :: l) l0)))
      else
       filt (mk_ev_S (!A))
         ((mapT (fun z : V => tripleT a z a1) l) @
            (listPd_fst_fix a (a0 :: l) l0)))).
case (dec_pdT_lem_snd (ev_dec V (! A))
           (tripleT a a0 a1)).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
unfold filt in H0;rewrite H0.
rewrite lgt_map_diff_eq_snd.
auto with * .
Qed.

Lemma proba_diff_mk_eq_mk_diff:forall (A:Event V)(l g:listT V)(h:listT W),
(Pr (listPd l g h) (!(mk_ev_F A)) =
Pr (listPd l g h) (mk_ev_F (! A)))%R.
unfold Pr;unfold Proba;intros.
elim l.
elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_diff_mk_eq_mk_diff.
auto.
Qed.


Lemma proba_diff_mk_eq_mk_diff_snd:
forall (A:Event V)(l g:listT V)(h:listT W),
(Pr (listPd l g h) (! (mk_ev_S A)) =
Pr (listPd l g h) (mk_ev_S (! A)))%R.
unfold Pr;unfold Proba.
intros;elim l.
elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_diff_mk_eq_mk_diff_snd.
auto.
Qed.


Lemma pr_diff_mk_eq_mk_diff:
forall (A:Event V)(l g:listT V)(h:listT W),
(pr (listPd l g h) (!(mk_ev_F A)) =
pr (listPd l g h) (mk_ev_F (! A)))%R.
intros.
unfold pr;unfold prob.
rewrite proba_diff_mk_eq_mk_diff.
auto.
Qed.

Lemma pr_diff_mk_eq_mk_diff_snd:
forall (A:Event V)(l g:listT V)(h:listT W),
(pr (listPd l g h) (!(mk_ev_S A)) =
pr (listPd l g h) (mk_ev_S (! A)))%R.
intros.
unfold pr;unfold prob.
rewrite proba_diff_mk_eq_mk_diff_snd.
auto.
Qed.

(*--------------- Event of type VxW to Event of type VxVxW ------------------*)

Lemma lgt_filt_mk_tr:forall (A : Event (prodT V W))(a0:W)(a1:V)(l:listT W),
(event_pred _ A (pairT a1 a0))->(lengthT
        (filt (mk_pdT_trd A) (mapT (fun z : W => tripleT a0 z a1) l)))=lengthT l.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_trd (ev_dec (prodT V W) A)
           (tripleT a0 a a1)).
simpl;intros.
auto with * . 
simpl;intro;intuition.
Qed.

Lemma lgt_filt_mk_tr_not:forall (A : Event (prodT V W))(a0:W)(a1:V)(l:listT W),
~(event_pred  _ A (pairT a1 a0))->lengthT
        (filt (mk_pdT_trd A)
           (mapT (fun z : W => tripleT a0 z a1) l))=0.
induction l.
simpl;auto.
simpl;intros.
case (dec_pdT_trd (ev_dec (prodT V W) A)
           (tripleT a0 a a1)).
simpl;intro;intuition.
simpl;intros.
auto with * . 
Qed.

Lemma lgt_list_fst_fix_trd_eq:forall (g:listT V)(h:listT W)(A : Event (prodT V W))(a:W),
lengthT
     (filt (mk_pdT_trd A) (listPd_fst_fix a h g))=(lengthT h)* 
(lengthT (filt A  (mapT (fun z : V => pairT z a) g))).
unfold Pr;unfold Proba.
intros;elim g.
elim h.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
case ( event_dec (prodT V W) A (pairT a0 a)).
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H;rewrite H.
rewrite lgt_filt_mk_tr.
rewrite N_lemma.eq_mult_S.
auto with * .
auto.
simpl;intros.
rewrite lgt_filt_app.
unfold filt in H;rewrite H.
rewrite lgt_filt_mk_tr_not.
auto with * .
auto.
Qed.
Lemma eq_pr_mk_trd:forall (g:listT V)(h l:listT W)(A : Event (prodT V W)),
(Pr (listPd h l g )
         (mk_pdT_trd  A))=(lengthT l)*(Pr (listTprod g h) A).
unfold Pr;unfold Proba.
intros;elim h.
elim l.
elim g.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_app.
rewrite lgt_list_fst_fix_trd_eq.
unfold Pr;unfold Proba.
rewrite Arith.Mult.mult_plus_distr_l. 
auto with * .
Qed.


Lemma  prod_mk_prod_trd :
    forall (A : Event (prodT V W))(l h:listT W)(g:listT V),
lengthT l<>0->lengthT h<>0->lengthT g<>0->
    pr (listTprod g l) A = pr (listPd l h g) (mk_pdT_trd A).
unfold pr;unfold prob.
intros.
rewrite <-listTprod_lengthT_ .
rewrite eq_pr_mk_trd.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite  Raxioms.Rmult_comm with (r1:=(Raxioms.INR (lengthT l))). 
rewrite Raxioms.Rmult_assoc.
rewrite Rmult_comm with (r2:=(Rmult (INR (lengthT l))
           (INR (lengthT g)))).
rewrite R_lemma.Rdiv_Rmult_simpl_.
rewrite lgt_listp.
rewrite RIneq.mult_INR.
auto with * .
auto with * .
generalize (R_lemma.Rmult_eq_0  (Raxioms.INR (lengthT l)) ( Raxioms.INR (lengthT g))).
intros;intuition.
Qed.
 

End pr_PdT.