Require Import listT.
Require Import prob.
Require Import ZArith.


Lemma le_inc :
 forall (V : Type) (l : listT V) (a : V) (A : Event V),
 A a -> InT a l -> 1 <= lengthT (filter V A l). 
simple induction l.
simpl in |- *; intros; intuition.
simpl in |- *; intros.
case (event_dec V A a).
simpl in |- *.
intro; auto with *.
intros.
elim H1.
intro.
rewrite H2 in n; intuition.
intro.
apply (H a0); intuition.
Qed.

Lemma eq_inc :
 forall (V : Type) (l g : listT V) (a : V) (A : Event V),
 A a ->
 lengthT (filter V A (appT l (consT a g))) =
 S (lengthT (filter V A (appT l g))).
simple induction l.
simpl in |- *; intros; intuition.
case (event_dec V A a).
simpl in |- *; intros; intuition.
simpl in |- *; intros; intuition.
simpl in |- *; intros.
case (event_dec V A a).
simpl in |- *; intros; intuition.
simpl in |- *; intros; intuition.
Qed.


Lemma inc_impl :
 forall (V W : Type) (u l : listT (prodT V W)) (A : Event (prodT V W))
   (a : prodT V W),
 A a ->
 inclT (consT a l) u ->
 exists t : listT (prodT V W),
   lengthT (filter (prodT V W) A u) = S (lengthT (filter (prodT V W) A t)).
simple induction u.
unfold inclT in |- *.
simpl in |- *; intros; intuition.
elim (H0 a).
intuition.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *; intro.
exists l; auto.
unfold inclT in H1; simpl in H1.
elim (H1 a0).
intros.
rewrite H2 in n; intuition.
intros.
apply H with (a := a0) (A := A) (l0 := l).
intuition.
unfold inclT in |- *; simpl in |- *.
intros.
elim H3.
intro.
rewrite <- H4; auto.
auto.
intuition.
Qed.


Lemma in_filt :
 forall (W : Type) (u : listT W) (A : Event W) (a : W),
 A a -> InT a u -> InT a (filter W A u).
simple induction u.
simpl in |- *.
auto with *.
simpl in |- *; intros.
case (event_dec W A a).
simpl in |- *; intros.
elim H1.
auto with *.
intro.
right; apply H; auto with *.
intro.
elim H1.
intro heq; rewrite heq in n; intuition.
apply H; auto with *.
Qed.



Lemma inT_filt :
 forall (W : Type) (t u : listT W) (A : Event W),
 incT t u -> incT (filter W A t) (filter W A u).
simple induction t.
simple induction u.
simpl in |- *.
auto with *.
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
simpl in H.
case (event_dec W A a).
simpl in |- *; intros.
split.
apply in_filt; intuition.
apply H; intuition.
intro; apply H; intuition.
Qed.



Lemma lgt_filt_app :
 forall (W : Type) (l g : listT W) (A : Event W),
 lengthT (filter W A (appT l g)) =
 lengthT (filter W A l) + lengthT (filter W A g).
simple induction l.
simpl in |- *; intros; auto with *.
simpl in |- *; intros.
case (event_dec W A a); simpl in |- *; intros; auto with *.
Qed.



Lemma lgt_listp_filt_cons_eq :
 forall (V W : Type) (g : listT W) (l : listT V) (a : V)
   (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (listTprod (consT a l) g)) =
 lengthT
   (filter (prodT V W) A
      (appT (mapT (fun z : W => pairT a z) g) (listTprod l g))).
simple induction g.
simpl in |- *.
intros; case l; auto with *.
simpl in |- *; intros.
case (event_dec (prodT V W) A (pairT a0 a)).
simpl in |- *; intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_app.
auto with *.
simpl in |- *; intros.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
auto with *.
Qed.


Lemma le_lgt_filt_app :
 forall (V W : Type) (g : listT W) (l : listT V) (r : listT (prodT V W))
   (a : V) (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (appT r (listTprod l g))) <=
 lengthT (filter (prodT V W) A (appT r (listTprod (consT a l) g))).
intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
auto with *.
Qed.

Lemma le_lgt_app_app :
 forall (V W : Type) (g : listT W) (l : listT V) (r w : listT (prodT V W))
   (a : V) (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (appT r (appT w (listTprod l g)))) <=
 lengthT (filter (prodT V W) A (appT r (appT w (listTprod (consT a l) g)))).
intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
auto with *.
Qed.

Lemma eq_lgt_cons :
 forall (V W : Type) (r w : listT (prodT V W)) (a : prodT V W) 
   (l : listT W) (l0 : listT V) (A : Event (prodT V W)),
 A a ->
 lengthT (filter (prodT V W) A (appT r (consT a (appT w (listTprod l0 l))))) =
 S (lengthT (filter (prodT V W) A (appT r (appT w (listTprod l0 l))))).
simple induction r.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *; auto with *.
intro; intuition.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *.
intro.
generalize (H w a l0 l1 A e).
intro; auto with *.
intro.
apply (H w a0 l0 l1 A H0).
Qed.

Lemma eq_lgt_cons2 :
 forall (V W : Type) (r w : listT (prodT V W)) (a : prodT V W) 
   (l : listT W) (l0 : listT V) (A : Event (prodT V W)),
 ~ A a ->
 lengthT (filter (prodT V W) A (appT r (consT a (appT w (listTprod l0 l))))) =
 lengthT (filter (prodT V W) A (appT r (appT w (listTprod l0 l)))).         
simple induction r.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
intro; intuition.
simpl in |- *; auto with *.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *.
intro.
generalize (H w a0 l0 l1 A H0).
intro; auto with *.
intro.
apply (H w a0 l0 l1 A H0).
Qed.


Lemma dec_ev : forall (V : Type) (A : Event V) (a : V), {A a} + {~ A a}.
intros.
elim A.
intros.
unfold dec_pred in event_dec.
simpl in |- *.
auto with *.
Qed.

Set Implicit Arguments.
Unset Strict Implicit.

Lemma le_app :
 forall (V W : Type) (r w : listT (prodT V W)) (a0 : V) 
   (l : listT W) (l0 : listT V) (A : Event (prodT V W)),
 S (lengthT (filter (prodT V W) A (appT r (listTprod l0 l)))) <=
 lengthT (filter (prodT V W) A (appT r (listTprod (consT a0 l0) l))) ->
 S (lengthT (filter (prodT V W) A (appT r (appT w (listTprod l0 l))))) <=
 lengthT (filter (prodT V W) A (appT r (appT w (listTprod (consT a0 l0) l)))).
intros.
induction  w as [| a w Hrecw].
simpl in |- *; intros; auto with *.
simpl in |- *; intros.
case (dec_ev (prodT V W) A a).
intro.
rewrite eq_lgt_cons; auto.
rewrite eq_lgt_cons; auto.
auto with *.
intro.
rewrite eq_lgt_cons2; auto.
rewrite eq_lgt_cons2; auto.
Qed.


Lemma inc_cons : forall (V : Type) (g : listT V) (a : V), incT g (consT a g).
simple induction g.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
split.
intuition.
apply incT_cons.
auto.
Qed.

Lemma inc_app_cons :
 forall (V : Type) (r g : listT V) (a : V),
 incT (appT r g) (appT r (consT a g)).
simple induction r.
simpl in |- *; intros.
apply inc_cons.
simpl in |- *; intros.
split; intuition.
apply incT_cons.
auto.
Qed.

Lemma le_app_cons :
 forall (V W : Type) (r g : listT (prodT V W)) (A : Event (prodT V W))
   (a : prodT V W),
 lengthT (filter (prodT V W) A (appT r g)) <=
 lengthT (filter (prodT V W) A (appT r (consT a g))).
intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
simpl in |- *.
case (event_dec (prodT V W) A a).
simpl in |- *; intro.
auto with *.
simpl in |- *; intro.
auto with *.
Qed.


Lemma le_lgt_InT :
 forall (V W : Type) (g : listT W) (a : V) (A : Event (prodT V W)) (c : W),
 InT c g ->
 A (pairT a c) ->
 1 <= lengthT (filter (prodT V W) A (mapT (fun z : W => pairT a z) g)).
simple induction g.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
case (event_dec (prodT V W) A (pairT a0 a)).
simpl in |- *; intros; auto with *.
intro.
elim H0.
intro heq; rewrite heq in n; intuition.
intro; apply H with c; auto with *.
Qed.

Lemma eq_S_plus_1 : forall n : nat, S n = n + 1.
intros.
auto with *.
Qed.

Lemma le_lgt_app_in :
 forall (V W : Type) (g : listT W) (l : listT V) (r : listT (prodT V W))
   (a : V) (A : Event (prodT V W)) (c : W),
 InT c g ->
 A (pairT a c) ->
 S (lengthT (filter (prodT V W) A (appT r (listTprod l g)))) <=
 lengthT (filter (prodT V W) A (appT r (listTprod (consT a l) g))).
intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
simpl in |- *.
rewrite
 plus_comm
           with
           (n := 
             lengthT (filter (prodT V W) A (mapT (fun z : W => pairT a z) g))).
rewrite eq_S_plus_1.
rewrite plus_assoc.
apply plus_le_compat.
auto with *.
apply le_lgt_InT with c; auto with *.
Qed.




Lemma le_lgt_cons :
 forall (W Zq:Type)(l : listT W) (a : W) 
   (g : listT Zq) (A : Event (prodT W Zq)) 
   (c d : Zq),
 InT c g ->
 A (pairT a c) ->
 S
   (lengthT
      (filter (prodT W Zq) A (listTprod l (consT d g)))) <=
 lengthT
   (filter (prodT W Zq) A
      (listTprod (consT a l) (consT d g))).
intros.
simpl.
case (event_dec (prodT W Zq) A (pairT a d)).
simpl;intros.
generalize
 (le_lgt_filt_app W Zq g l
    (mapT (fun z :W => pairT z d) l) a A).
intros.
auto with *.
simpl in |- *; intros.
apply le_lgt_app_in with (c := c); auto.
Qed.


Lemma le_lgt_app_ :
 forall (W : Type) (l g : listT W) (A : Event W),
 lengthT (filter W A g) <= lengthT (filter W A (appT l g)).
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec W A a).
simpl in |- *; intro; auto with *.
simpl in |- *; intro; auto with *.
Qed.

Lemma le_lgt_impl_lgt_app :
 forall (W : Type) (l g h : listT W) (A : Event W),
 lengthT (filter W A g) <= lengthT (filter W A h) ->
 lengthT (filter W A (appT l g)) <= lengthT (filter W A (appT l h)).
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec W A a).
simpl in |- *; intro; auto with *.
simpl in |- *; intro; auto with *.
Qed.

Lemma le_lgt_list_cons :
 forall (V W : Type) (g : listT W) (l : listT V) (a : V)
   (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (listTprod l g)) <=
 lengthT (filter (prodT V W) A (listTprod (consT a l) g)).
simple induction g.
simpl in |- *.
auto.
simpl in |- *; intros.
case (event_dec (prodT V W) A (pairT a0 a)).
simpl in |- *; intro.
generalize
 (le_lgt_impl_lgt_app (mapT (fun z : V => pairT z a) l0) (H l0 a0 A)).
intro; auto with *.
simpl in |- *; intros.
generalize
 (le_lgt_impl_lgt_app (mapT (fun z : V => pairT z a) l0) (H l0 a0 A)).
intro; auto with *.
Qed.








Lemma le_app_list :
 forall (V W : Type) (w : listT (prodT V W)) (l : listT V) 
   (g : listT W) (a : V) (B : Event W) (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (listTprod (consT a l) g)) <=
 lengthT (filter W B g) + lengthT (filter (prodT V W) A (listTprod l g)) ->
 lengthT (filter (prodT V W) A (appT w (listTprod (consT a l) g))) <=
 lengthT (filter W B g) +
 lengthT (filter (prodT V W) A (appT w (listTprod l g))).
simple induction w.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *.
rewrite <- plus_n_Sm.
intro.
generalize (H l0 g a0 B A H0).
intros; auto with *.
intro.
generalize (H l0 g a0 B A H0).
intros; auto with *.
Qed.

Lemma le_lgt_filter_cons :
 forall (V W : Type) (l : listT V) (g : listT W) (a : V)
   (A : Event (prodT V W))
   (dec_ev_W : dec_pred W (fun z : W => A (pairT a z))),
 lengthT (filter (prodT V W) A (listTprod (consT a l) g)) <=
 lengthT (filter W (Build_Event W (fun z : W => A (pairT a z)) dec_ev_W) g) +
 lengthT (filter (prodT V W) A (listTprod l g)).
simple induction g.
simpl in |- *; intros.
auto with *.
simpl in |- *; intros.
case (event_dec (prodT V W) A (pairT a0 a)).
case (dec_ev_W a).
simpl in |- *; intros.
generalize (H a0 A dec_ev_W).
intro.
generalize (le_app_list (mapT (fun z : V => pairT z a) l) H0).
intro.
auto with *.
intro; intuition.
intro.
case (dec_ev_W a).
intro; intuition.
simpl in |- *; intros.
generalize (H a0 A dec_ev_W).
intro.
apply (le_app_list (mapT (fun z : V => pairT z a) l) H0).
Qed.




Lemma eq_app_list :
 forall (V W : Type) (w : listT (prodT V W)) (l : listT V) 
   (g : listT W) (a : V) (B : Event W) (A : Event (prodT V W)),
 lengthT (filter (prodT V W) A (listTprod (consT a l) g)) =
 lengthT (filter W B g) + lengthT (filter (prodT V W) A (listTprod l g)) ->
 lengthT (filter (prodT V W) A (appT w (listTprod (consT a l) g))) =
 lengthT (filter W B g) +
 lengthT (filter (prodT V W) A (appT w (listTprod l g))).
simple induction w.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec (prodT V W) A a).
simpl in |- *.
rewrite <- plus_n_Sm.
intro.
generalize (H l0 g a0 B A H0).
intros; auto with *.
intro.
generalize (H l0 g a0 B A H0).
intros; auto with *.
Qed.



Lemma eq_lgt_app :
 forall (V : Type) (A B : Event V) (w l : listT V),
 (forall a : V, A a -> B a) ->
 (forall a : V, B a -> A a) ->
 lengthT (filter V A l) = lengthT (filter V B l) ->
 lengthT (filter V A (appT w l)) = lengthT (filter V B (appT w l)).
simple induction w.
simpl in |- *; intros; auto.
simpl in |- *; intros.
case (event_dec V A a).
case (event_dec V B a).
simpl in |- *; intros; auto with *.
intros.
assert (~ A a); intuition.
case (event_dec V B a).
intros.
assert (~ B a); intuition.
auto with *.
Qed.



Lemma indep_listTprod :forall (V:Type) (l1 l2 : listT V) (A B : Event V),
 lengthT
   (filter (prodT V V)
      (EventInter (prodT V V) (mk_ev_fst V A) (mk_ev_snd V B))
      (listTprod l1 l2)) = lengthT (filter V A l1) * lengthT (filter V B l2).
simple induction l1.
simple induction l2.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
rewrite listp_nil.
simpl in |- *; auto.
simpl in |- *; intros.
rewrite lgt_listp_filt_cons_eq.
case (event_dec V A a).
simpl in |- *.
intro.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_inter.
auto.
auto.
simpl in |- *; intros.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_inter_not.
auto with *.
auto.
Qed.




Lemma lgt_map :
 forall (V : Type) (l : listT V) (A : Event V) (a : V),
 A a ->
 lengthT
   (filter (prodT V V) (mk_ev_fst V A) (mapT (fun z : V => pairT a z) l)) =
 lengthT l.
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.


Lemma lgt_map_l :
 forall (V : Type) (l : listT V) (A : Event V) (a : V),
 A a ->
 lengthT
   (filter (prodT V V) (mk_ev_snd V A) (mapT (fun z : V => pairT z a) l)) =
 lengthT l.
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.

Unset Strict Implicit.
Set Implicit Arguments.

Lemma lgt_map_not :
 forall (V : Type) (l : listT V) (A : Event V) (a : V),
 ~ A a ->
 lengthT
   (filter (prodT V V) (mk_ev_fst V A) (mapT (fun z : V => pairT a z) l)) =
 0.
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.

Lemma lgt_map_not_l :
 forall (V : Type) (l : listT V) (A : Event V) (a : V),
 ~ A a ->
 lengthT
   (filter (prodT V V) (mk_ev_snd V A) (mapT (fun z : V => pairT z a) l)) =
 0.
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.




Lemma lgt_filt_mk_fst:
 forall (V : Type) (l1 l2 : listT V) (A : Event V),
 lengthT (filter V A l1) * lengthT l2 =
 lengthT (filter (prodT V V) (mk_ev_fst V A) (listTprod l1 l2)).
simple induction l1.
simple induction l2.
simpl in |- *.
auto.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec V A a).
simpl in |- *.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
simpl in |- *; intros.
rewrite lgt_map.
rewrite H.
auto with *.
auto.
simpl in |- *; intros.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_map_not.
auto with *.
auto.
Qed.


Lemma lgt_filt_mk_snd :
 forall (V : Type) (l2 l1 : listT V) (B : Event V),
 lengthT (filter V B l2) * lengthT l1 =
 lengthT (filter (prodT V V) (mk_ev_snd V B) (listTprod l1 l2)).
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.
rewrite lgt_map_l.
auto with *.
auto.
simpl in |- *; intros.
rewrite lgt_filt_app.
rewrite Hrecl2.
rewrite lgt_map_not_l.
auto with *.
auto.
Qed.

Require Import Reals.
Require Import Logic_Type.
Require Import listT.
Require Import R_lemma.

Lemma indep_ev :
 forall (V : Type) (l1 l2 : listT V) (A B : Event V),
 INR (lengthT l1) <> 0%R ->
 INR (lengthT l2) <> 0%R ->
 indep _ (listTprod l1 l2) (mk_ev_fst V A)
   (mk_ev_snd V B).
intros.
unfold indep in |- *.
unfold prob in |- *.
replace (Proba (prodT V V) (listTprod l1 l2) (mk_ev_fst V A)) with
 (Proba V l1 A * lengthT l2).
replace (Proba (prodT V V) (listTprod l1 l2) (mk_ev_snd V B)) with
 (Proba V l2 B * lengthT l1).
replace (lengthT (listTprod l1 l2)) with (lengthT l1 * lengthT l2).
unfold Proba in |- *.
apply Rewr_Rdiv_mult.
auto with *.
auto with *.
apply indep_listTprod.
apply listTprod_lengthT.
unfold Proba in |- * .
apply lgt_filt_mk_snd.
unfold Proba in |- * .
apply lgt_filt_mk_fst. 
Qed.


Lemma eq_fst_map:forall (V:Type)(A : Event V) (a:V)(l:(listT V)),(lengthT
        (filter (prodT V V) (mk_ev_fst V A)
           (mapT (fun z : V=> pairT z a) l)))= (lengthT (filter V A l)).
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.

Section eq_pr.
Variable V:Type.
Variable Ef Eg:listT V.
Hypotheses lgt_Ef:lengthT Ef<>0.
Hypotheses lgt_Eg:lengthT Eg<>0.


Lemma eq_pr_mkfst:forall (A : Event V),(Proba (prodT V V) (listTprod Ef Eg)
         (mk_ev_fst V A))=(lengthT Eg)*(Proba V Ef A).
unfold Proba.
elim Ef.
elim Eg.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim Eg.
simpl;intros;auto.
simpl;intros a0 l0.
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.
rewrite eq_fst_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.
rewrite eq_fst_map.
auto with *.
Qed.

Definition pr_f := prob V Ef.
Definition pr_g := prob V Eg.
Definition pr_fg := prob (prodT V V) (listTprod Ef Eg).
Definition pr_cond_f := prob_cond V Ef.
Definition pr_cond_g := prob_cond V Eg.
Definition pr_cond_fg :=
  prob_cond (prodT V V) (listTprod Ef Eg).

Lemma  prod_mk_prod_ev_fst :
    forall A : Event V,
    pr_f A = pr_fg (mk_ev_fst V A).
unfold pr_f;unfold pr_fg.
unfold prob.
intros.
rewrite <-listTprod_lengthT.
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 Eg))).
rewrite RIneq.Rinv_mult_distr.
rewrite Rmult_comm with (r1:=(Rinv (INR (lengthT Ef)))).
rewrite<- Rmult_assoc.
replace (INR (Proba V Ef A) * INR (lengthT Eg) * / INR (lengthT Eg) *
    / INR (lengthT Ef))%R with (INR (Proba V Ef A) * (INR (lengthT Eg) * / INR (lengthT Eg) )*
    / INR (lengthT Ef))%R.
rewrite Rmult_comm with (r1:=(INR (lengthT Eg))).
rewrite <-RIneq.Rinv_l_sym with (r:=INR (lengthT Eg)).
replace  (INR (Proba V Ef A) * 1 * / INR (lengthT Ef))%R with (INR (Proba V Ef A) * (1 * / INR (lengthT Ef)))%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.




Lemma lgt_listp_not_eq:forall (T:Type)(E G:(listT T)),lengthT E <> 0->  lengthT G <> 0->lengthT (listTprod E G) <> 0.
induction E;induction G.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.



Lemma  prod_mk_prod_ev_fst_diff :
    forall A : Event V,
    pr_f (Eventdiff V A) =
    pr_fg
      (Eventdiff (prodT V V)
         (mk_ev_fst V A)).
intros.
unfold pr_f.
rewrite prob_diff_eq_min_1.
rewrite prod_mk_prod_ev_fst.
unfold pr_fg.
rewrite prob_diff_eq_min_1.
auto with *.
apply lgt_listp_not_eq;auto.
auto.
Qed.





Lemma eq_snd_map:forall (A : Event V) (a:V)(l:(listT V)),(lengthT
        (filter (prodT V V) (mk_ev_snd V A)
           (mapT (fun z : V => pairT a z) l)))= (lengthT (filter V A l)).
induction l.
simpl;intros;auto.
simpl;intros.
case ( dec_pred_snd  V V A (ev_dec V A) (pairT a a0)).
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.

Lemma eq_snd: forall (A : Event V) (a:V)(l:(listT V)),(A a)->(lengthT
        (filter (prodT V V) (mk_ev_snd V A)
           (mapT (fun z : V  => pairT z a) l)))=(lengthT l).
induction l.
simpl;intros;auto.
simpl;intros.
case ( dec_pred_snd V V A (ev_dec V A) (pairT a0 a)).
simpl;intros.
auto with *.
simpl;intros;intuition.
Qed.
Lemma not_eq_snd: forall (A : Event V) (a:V)(l:(listT V)),~(A a)->(lengthT
        (filter (prodT V V) (mk_ev_snd V A)
           (mapT (fun z : V  => pairT z a) l)))=(0).
induction l.
simpl;intros;auto.
simpl;intros.
case ( dec_pred_snd  V V A (ev_dec V A) (pairT a0 a)).
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.

Lemma eq_S_simpl:forall a b c:nat,S (a+(b+a*c))=S (b+a*S c).
intros.
rewrite <-mult_n_Sm.
rewrite plus_comm .
auto with *.
Qed.
 
Lemma eq_pr_mksnd:forall A : Event V,(Proba (prodT V V) (listTprod Ef Eg)
         (mk_ev_snd V A))=(lengthT Ef)*(Proba V Eg A).
unfold Proba.
elim Ef.
elim Eg.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
elim Eg.
simpl;intros;auto.
simpl;intros a0 l0.
case (  dec_pred_snd V V A (ev_dec V A) (pairT a a0)).
case (event_dec V A a0 ).
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
rewrite eq_snd.
apply eq_S_simpl .
auto.
simpl;intros;intuition.
case (event_dec V A a0).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite H0.
rewrite not_eq_snd.
auto.
auto.
Qed.


Lemma prod_mk_prod_ev_snd:    forall A : Event V,
    pr_g  A =pr_fg (mk_ev_snd V A).
unfold pr_g;unfold pr_fg.
unfold prob.
intros.
rewrite <-listTprod_lengthT.
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 Ef))).
rewrite RIneq.Rinv_mult_distr.
rewrite<- Rmult_assoc.
replace  (INR (Proba V Eg A) * INR (lengthT Ef) * / INR (lengthT Ef) *
    / INR (lengthT Eg))%R with (INR (Proba V Eg A) *( INR (lengthT Ef) * / INR (lengthT Ef)) *
    / INR (lengthT Eg))%R .
rewrite Rmult_comm with (r1:=(INR (lengthT Ef))).
rewrite <-RIneq.Rinv_l_sym with (r:=INR (lengthT Ef)).
replace  (INR (Proba V Eg A) * 1 * / INR (lengthT Eg))%R with (INR (Proba V Eg A) * (1 * / INR (lengthT Eg)))%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.

Lemma prod_mk_prod_ev_snd_diff :
    forall A : Event V,
    pr_g (Eventdiff V A) =
    pr_fg
      (Eventdiff (prodT V V)
         (mk_ev_snd V A)).
intros.
unfold pr_g.
rewrite prob_diff_eq_min_1.
rewrite prod_mk_prod_ev_snd.
unfold pr_fg.
rewrite prob_diff_eq_min_1.
auto with *.
apply lgt_listp_not_eq;auto.
auto.
Qed.

End eq_pr.


Lemma lgt_filt_listp :
 forall (V : Type) (l1 l2 : listT V) (A : Event V),
 lengthT (filter V A l1) * lengthT l2 =
 lengthT (filter (prodT V V) (mk_ev_fst V A) (listTprod l1 l2)).
simple induction l1.
simple induction l2.
simpl in |- *.
auto.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
case (event_dec V A a).
simpl in |- * .
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
simpl in |- *; intros.
rewrite lgt_filt_map.
rewrite H.
auto with *.
auto.
simpl in |- *; intros.
rewrite lgt_listp_filt_cons_eq.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_map_not.
auto with *.
auto.
Qed.



Lemma indep_ev_:
 forall (V : Type) (l1 l2 : listT V) (A B : Event V),
 Raxioms.INR (lengthT l1) <> Rdefinitions.R0 ->
 Raxioms.INR (lengthT l2) <> Rdefinitions.R0 ->
 indep  (prodT V V) (listTprod l1 l2) (mk_ev_fst V A)
   (mk_ev_snd V  B).
intros.
unfold indep in |- *.
unfold prob in |- *.
replace (Proba (prodT V V) (listTprod l1 l2) (mk_ev_fst  V A)) with
 (Proba V l1 A * lengthT l2).
replace (Proba (prodT V V) (listTprod l1 l2) (mk_ev_snd V B)) with
 (Proba V l2 B * lengthT l1).
replace (lengthT (listTprod l1 l2)) with (lengthT l1 * lengthT l2).
unfold Proba in |- * .
apply R_lemma.Rewr_Rdiv_mult.
auto with * .
auto with * .
apply indep_listTprod.
apply listTprod_lengthT.
generalize (eq_pr_mksnd l1 l2  B);unfold Proba;intro;auto with *.
rewrite H1;auto with *.
unfold Proba in |- * .
apply (lgt_filt_listp l1 l2 A).
Qed.


Lemma indep_ev_pdT :forall (V W:Type)(A B : Event W)(l g:listT W)(h:listT V),
lengthT l<>0->lengthT g<>0->lengthT h<>0->
 indep (PdT W W V)   (listPd l g h) (mk_pdT_ev_fst V A)
   (mk_pdT_ev_snd  V B).
intros.
unfold indep .
generalize prod_mk_pdT_ev_snd.
generalize prod_mk_pdT_ev_fst.
intros.
rewrite<- H2;auto with * .
rewrite <-H3;auto with * .
rewrite prod_mk_pdT_ev_inter;auto with * . 
generalize indep_ev_ .
unfold indep.
intro.
rewrite H4;auto with * .
rewrite <-prod_mk_ev_fst;auto with * .
rewrite <-prod_mk_ev_snd;auto with * .
Qed.