Library corde
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq finfun path.
Require Import fintype finset tuple div zmodp bigop ssralg perm fingroup rat.
Import GRing.Theory.
Section Corde.
(******************************************************************************)
(* *)
(* *)
(* MODÉLISATION *)
(* *)
(* *)
(******************************************************************************)
(* Un ensemble de noeuds est une permutation dont tous les cycles sont de *)
(* longueur 2 *)
Definition is_node n :=
[set p | [forall i : 'I_n, ((p : 'S_n) (p i) == i) && (p i != i)]].
Notation " 'N[ n ] " := (@is_node n).
Lemma is_nodeK n (p : 'S_n) i : p \in 'N[n] -> p (p i) = i.
Lemma is_node_diff n (p : 'S_n) i : p \in 'N[n] -> p i != i.
Lemma is_node_flip n p i j : p \in 'N[n] -> p i = j -> p j = i.
(* Une configuration valide est une paire de permutation de 2-cycles *)
Definition config n := ('S_n * 'S_n)%type.
Definition cvalid n : {set config n} := setX 'N[n] 'N[n].
Notation " 'N2[ n ] " := (cvalid n).
(* On suit la corde i pour m.*2 suivant la config c *)
Fixpoint follow m n (c : config n) x :=
if m is m1.+1 then x :: c.1 x :: follow m1 c (c.2 (c.1 x)) else [::].
(* On obtient bien une liste de longuer 2m *)
Lemma size_follow m n (c : config n) x : size (follow m c x) = m.*2.
(* Les cordes sont toutes liées entre elles, si en suivant la corde 0 on *)
(* obtient toutes les cordes *)
Definition c2l n (c : config n.+1.*2) : seq 'I_n.+1.*2 := follow n.+1 c 0%R.
Definition one_cycle n := [set c | uniq (@c2l n c)].
Notation " 'O[ n ] " := (@one_cycle n).
(******************************************************************************)
(* *)
(* NOMBRE DE CONFIGURATIONS *)
(* *)
(******************************************************************************)
(* Les ordinaux plus petits qu'une certaine valeur *)
Definition lordinal n k := [set i | (i : 'I_n) < k].
Lemma card_lordinal n k : k <= n -> #|lordinal n k| = k.
(* Enlever les deux cycles (i, p i) et (j, p j) *)
Definition swap_node n (p : 'S_n) i j :=
(p * tperm i (p i) * tperm j (p j) * tperm (p i) (p j))%g.
Lemma swap_nodeL n (p : 'S_n) i j :
p i != i -> p (p j) = j -> i != j -> swap_node p i j i = i.
Lemma swap_nodeLp n (p : 'S_n) i j :
p i != j -> p (p i) = i -> i != j -> swap_node p i j (p i) = p j.
Lemma swap_nodeR n (p : 'S_n) i j :
p j != j -> p (p j) = j -> i != j -> swap_node p i j j = j.
Lemma swap_nodeRp n (p : 'S_n) i j :
p i != j -> p (p j) = j -> i != j -> swap_node p i j (p j) = p i.
Lemma swap_nodeD n (p : 'S_n) i j k :
p (p i) = i -> p (p j) = j ->
k \notin [:: i; j; p i; p j] -> swap_node p i j k = p k.
(* Rajouter deux cycles (i, k) et (j, p k) *)
Definition unswap_node n (p : 'S_n) i j k :=
(p * tperm i (p k) * tperm j k * tperm k (p k))%g.
Lemma unswap_nodeL n (p : 'S_n) i j k :
p i = i -> p j = j -> p k != k -> unswap_node p i j k i = k.
Lemma unswap_nodeR n (p : 'S_n) i j k :
i != j -> p j = j -> p k != k -> unswap_node p i j k j = p k.
Lemma unswap_nodeM n (p : 'S_n) i j k :
i != j -> p i = i -> p j = j -> p k != k -> unswap_node p i j k k = i.
Lemma unswap_nodeMp n (p : 'S_n) i j k :
i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
unswap_node p i j k (p k) = j.
Lemma unswap_nodeD n (p : 'S_n) i j k l :
p i = i -> p j = j -> p (p k) = k ->
l \notin [:: i; j; k; p k] -> unswap_node p i j k l = p l.
Lemma swap_nodeK n (p : 'S_n) i j :
i != j -> p i != i -> p (p i) = i -> p j != j -> p (p j) = j ->
unswap_node (swap_node p i j) i j (p i) = p.
Lemma unswap_nodeK n (p : 'S_n) i j k:
i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
swap_node (unswap_node p i j k) i j = p.
(* Ajouter les deux cycles (i, t.2) et (i + 1, p t.2)) *)
Definition pI2S m (i : 'I_m.+2) (t : 'S_m.+2 * 'I_m.+2) : 'S_m.+2 :=
unswap_node t.1 (i + 1)%R i t.2.
(* Enlever les deux cycles (i, p i) et (i + 1, p (i + 1)) *)
Definition S2pI m (i : 'I_m.+2) (p : 'S_m.+2) : 'S_m.+2 * 'I_m.+2 :=
(swap_node p (i + 1)%R i, p (i + 1)%R).
(* Version de is_node paramétré pour permettre une preuve par induction *)
Definition is_nodeL m k :=
[set p |
[forall i : 'I_m, if i < k.*2 then ((p : 'S_m) (p i) == i) && (p i != i)
else p i == i]].
Notation " 'N[ n , k ] " := (@is_nodeL n k).
Lemma is_nodeLE n : 'N[n.*2,n] = 'N[n.*2].
Lemma PPN n k p i : p \in 'N[n, k] -> p (p i) = i.
Lemma PDN n k p (i : 'I_n) : p \in 'N[n, k] -> i < k.*2 -> p i != i.
Lemma PEN n k p (i : 'I_n) : p \in 'N[n, k] -> k.*2 <= i -> p i = i.
Lemma PLN n k p (i : 'I_n) : p \in'N[n, k] -> i < k.*2 -> p i < k.*2.
Lemma ISE n (i: 'I_n.+2) : i <= n -> (i + 1)%R = i.+1 :> nat.
Lemma ISDE n (i: 'I_n.+2) : i <= n -> (i + 1)%R != i.
(* Sp2I est bijectif *)
Lemma S2pIK n k (i : 'I_n.+2) :
i < k.*2.+1 <= n.+1 -> {in 'N[n.+2, k.+1], (pI2S i) \o (S2pI i) =1 id}.
(* pI2S est bijectif *)
Lemma pI2SK n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
{in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1), (S2pI i) \o (pI2S i) =1 id}.
(* L'image de S2pI (k décroit) *)
Lemma subset_S2pI n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
[set S2pI i p | p in 'N[n.+2, k.+1]]
\subset setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1).
(* L'image de p2SI (k croit) *)
Lemma subset_pI2S n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
[set pI2S i t | t in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1)]
\subset'N[n.+2, k.+1].
(* Cardinalité des permutations dont tous les cycles sont de longueur 2 *)
(* On fait la preuve par induction en enlevant deux cycles à la fois *)
Lemma card_is_node n : #|'N[n.+1.*2]| = \prod_(i < n.+1) i.*2.+1.
(* Cardinal des configurations *)
Lemma card_cvalid n : #|'N2[n.+1.*2]| = (\prod_(i < n.+1) i.*2.+1) ^ 2.
Fact card_cvalid6 : #|'N2[6]| = 15 ^ 2.
(******************************************************************************)
(* *)
(* NOMBRE DE CONFIGURATIONS A 1 CYCLE *)
(* *)
(******************************************************************************)
(* Promouvoir une fonction en une permutation *)
Definition perm_of n (f : {ffun 'I_n.+1 -> 'I_n.+1}) : 'S_n.+1 :=
odflt 1%g [pick p | f == (pval p)].
Lemma perm_ofE n (f: {ffun 'I_n.+1 -> _}) : injective f -> perm_of f =1 f.
Lemma oddI_pre n (i : 'I_n.+2) : ~~ odd n -> odd (i - 1)%R = ~~ odd i.
Lemma oddIS n (i : 'I_n.+2) : ~~ odd n -> odd (i + 1)%R = ~~ odd i.
(* Traduire une configuration en une permutation en utilisant la liste S2l *)
Definition c2p n (c : config n.+1.*2) :=
perm_of ([ffun n : 'I_ _ => nth 0%R (c2l c) n]).
(* Récupération de la première permutation de la configuration *)
Definition fun_permL n (p : 'S_n.+2) :=
[ffun i : 'I_n.+2 =>
let k := p^-1%g i in
if odd k then p (k - 1)%R else p (k + 1)%R].
Lemma fun_permLK n (p : 'S_n.+2) i :
~~ odd n -> fun_permL p (fun_permL p i) = i.
Lemma injective_permL n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permL p).
Lemma fun_permLF n (p : 'S_n.+2) i : ~~ odd n -> fun_permL p i != i.
(* Récupération de la deuxième permutation de la configuration *)
Definition fun_permR n (p : 'S_n.+2) :=
[ffun i : 'I_n.+2 =>
let k := p^-1%g i in
if odd k then p (k + 1)%R else p (k - 1)%R].
Lemma fun_permRK n (p : 'S_n.+2) i :
~~ odd n -> fun_permR p (fun_permR p i) = i.
Lemma injective_permR n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permR p).
Lemma fun_permRF n (p : 'S_n.+2) i : ~~ odd n -> fun_permR p i != i.
(* Traduire une permutation telle que p 0 = 0 en une configuration *)
Definition p2c n (p: 'S_n.+2) : config n.+2 :=
(perm_of (fun_permL p), perm_of (fun_permR p)).
(* Permutation qui valent 0 en 0 *)
Definition perm_fix0 n : pred 'S_n.+1 := perm_on [set~ ord0].
Notation " 'F[ n ] " := (@perm_fix0 n).
Lemma perm_fix0P n p : p \in @perm_fix0 n = (p 0%R == 0%R).
Lemma c2l_codom n (p: 'S_n.+1.*2) : p 0%R = 0%R -> c2l (p2c p) = codom p.
Lemma card_perm_fix0 n : #|'F[n]| = n`!.
Lemma imp2c n: [set p2c p | p in 'F[n.*2.+1]] \subset 'N2[(n.+1).*2] :&: 'O[n].
Lemma imc2p n: [set c2p c | c in 'N2[(n.+1).*2] :&: 'O[n]] \subset 'F[n.*2.+1].
Lemma p2SK n : {in 'F[n.*2.+1], (@c2p _) \o (@p2c n.*2) =1 id}.
Lemma I_preE n (i: 'I_n.+2) : 0 < i -> (i - 1)%R = i.-1 :> nat.
Lemma c2lLE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.1) :
((forall i, p (p i) = i) ->
p (c2l c)`_i = (c2l c)`_(if odd i then (i - 1) else (i + 1)))%R.
Lemma c2lRE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.2) :
((forall i, p (p i) = i) -> (forall i, p i != i) -> uniq (c2l c) ->
p (c2l c)`_i = (c2l c)`_(if odd i then (i + 1) else (i - 1)))%R.
Lemma S2pK n : {in 'N2[n.+1.*2] :&: 'O[n], (@p2c n.*2) \o (@c2p _) =1 id}.
Lemma card_N2O n : #|'N2[n.+1.*2] :&: 'O[n]| = n.*2.+1 `!.
(******************************************************************************)
(* *)
(* PROBABILITÉ *)
(* *)
(******************************************************************************)
Open Scope ring_scope.
(* Le rapport entre tous les configurations de noeuds avec un cycle et toutes *)
(* les configurations *)
Definition Proba n : rat := #|'N2[n.+1.*2] :&: 'O[n]|%:R / #|'N2[n.+1.*2]|%:R.
Lemma ProbaE n : Proba n = n.*2.+1 `!%:R / ((\prod_(i < n.+1) i.*2.+1) ^2)%:R.
Lemma result : Proba 2 = 8%:R / 15%:R.
End Corde.
Require Import fintype finset tuple div zmodp bigop ssralg perm fingroup rat.
Import GRing.Theory.
Section Corde.
(******************************************************************************)
(* *)
(* *)
(* MODÉLISATION *)
(* *)
(* *)
(******************************************************************************)
(* Un ensemble de noeuds est une permutation dont tous les cycles sont de *)
(* longueur 2 *)
Definition is_node n :=
[set p | [forall i : 'I_n, ((p : 'S_n) (p i) == i) && (p i != i)]].
Notation " 'N[ n ] " := (@is_node n).
Lemma is_nodeK n (p : 'S_n) i : p \in 'N[n] -> p (p i) = i.
Lemma is_node_diff n (p : 'S_n) i : p \in 'N[n] -> p i != i.
Lemma is_node_flip n p i j : p \in 'N[n] -> p i = j -> p j = i.
(* Une configuration valide est une paire de permutation de 2-cycles *)
Definition config n := ('S_n * 'S_n)%type.
Definition cvalid n : {set config n} := setX 'N[n] 'N[n].
Notation " 'N2[ n ] " := (cvalid n).
(* On suit la corde i pour m.*2 suivant la config c *)
Fixpoint follow m n (c : config n) x :=
if m is m1.+1 then x :: c.1 x :: follow m1 c (c.2 (c.1 x)) else [::].
(* On obtient bien une liste de longuer 2m *)
Lemma size_follow m n (c : config n) x : size (follow m c x) = m.*2.
(* Les cordes sont toutes liées entre elles, si en suivant la corde 0 on *)
(* obtient toutes les cordes *)
Definition c2l n (c : config n.+1.*2) : seq 'I_n.+1.*2 := follow n.+1 c 0%R.
Definition one_cycle n := [set c | uniq (@c2l n c)].
Notation " 'O[ n ] " := (@one_cycle n).
(******************************************************************************)
(* *)
(* NOMBRE DE CONFIGURATIONS *)
(* *)
(******************************************************************************)
(* Les ordinaux plus petits qu'une certaine valeur *)
Definition lordinal n k := [set i | (i : 'I_n) < k].
Lemma card_lordinal n k : k <= n -> #|lordinal n k| = k.
(* Enlever les deux cycles (i, p i) et (j, p j) *)
Definition swap_node n (p : 'S_n) i j :=
(p * tperm i (p i) * tperm j (p j) * tperm (p i) (p j))%g.
Lemma swap_nodeL n (p : 'S_n) i j :
p i != i -> p (p j) = j -> i != j -> swap_node p i j i = i.
Lemma swap_nodeLp n (p : 'S_n) i j :
p i != j -> p (p i) = i -> i != j -> swap_node p i j (p i) = p j.
Lemma swap_nodeR n (p : 'S_n) i j :
p j != j -> p (p j) = j -> i != j -> swap_node p i j j = j.
Lemma swap_nodeRp n (p : 'S_n) i j :
p i != j -> p (p j) = j -> i != j -> swap_node p i j (p j) = p i.
Lemma swap_nodeD n (p : 'S_n) i j k :
p (p i) = i -> p (p j) = j ->
k \notin [:: i; j; p i; p j] -> swap_node p i j k = p k.
(* Rajouter deux cycles (i, k) et (j, p k) *)
Definition unswap_node n (p : 'S_n) i j k :=
(p * tperm i (p k) * tperm j k * tperm k (p k))%g.
Lemma unswap_nodeL n (p : 'S_n) i j k :
p i = i -> p j = j -> p k != k -> unswap_node p i j k i = k.
Lemma unswap_nodeR n (p : 'S_n) i j k :
i != j -> p j = j -> p k != k -> unswap_node p i j k j = p k.
Lemma unswap_nodeM n (p : 'S_n) i j k :
i != j -> p i = i -> p j = j -> p k != k -> unswap_node p i j k k = i.
Lemma unswap_nodeMp n (p : 'S_n) i j k :
i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
unswap_node p i j k (p k) = j.
Lemma unswap_nodeD n (p : 'S_n) i j k l :
p i = i -> p j = j -> p (p k) = k ->
l \notin [:: i; j; k; p k] -> unswap_node p i j k l = p l.
Lemma swap_nodeK n (p : 'S_n) i j :
i != j -> p i != i -> p (p i) = i -> p j != j -> p (p j) = j ->
unswap_node (swap_node p i j) i j (p i) = p.
Lemma unswap_nodeK n (p : 'S_n) i j k:
i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
swap_node (unswap_node p i j k) i j = p.
(* Ajouter les deux cycles (i, t.2) et (i + 1, p t.2)) *)
Definition pI2S m (i : 'I_m.+2) (t : 'S_m.+2 * 'I_m.+2) : 'S_m.+2 :=
unswap_node t.1 (i + 1)%R i t.2.
(* Enlever les deux cycles (i, p i) et (i + 1, p (i + 1)) *)
Definition S2pI m (i : 'I_m.+2) (p : 'S_m.+2) : 'S_m.+2 * 'I_m.+2 :=
(swap_node p (i + 1)%R i, p (i + 1)%R).
(* Version de is_node paramétré pour permettre une preuve par induction *)
Definition is_nodeL m k :=
[set p |
[forall i : 'I_m, if i < k.*2 then ((p : 'S_m) (p i) == i) && (p i != i)
else p i == i]].
Notation " 'N[ n , k ] " := (@is_nodeL n k).
Lemma is_nodeLE n : 'N[n.*2,n] = 'N[n.*2].
Lemma PPN n k p i : p \in 'N[n, k] -> p (p i) = i.
Lemma PDN n k p (i : 'I_n) : p \in 'N[n, k] -> i < k.*2 -> p i != i.
Lemma PEN n k p (i : 'I_n) : p \in 'N[n, k] -> k.*2 <= i -> p i = i.
Lemma PLN n k p (i : 'I_n) : p \in'N[n, k] -> i < k.*2 -> p i < k.*2.
Lemma ISE n (i: 'I_n.+2) : i <= n -> (i + 1)%R = i.+1 :> nat.
Lemma ISDE n (i: 'I_n.+2) : i <= n -> (i + 1)%R != i.
(* Sp2I est bijectif *)
Lemma S2pIK n k (i : 'I_n.+2) :
i < k.*2.+1 <= n.+1 -> {in 'N[n.+2, k.+1], (pI2S i) \o (S2pI i) =1 id}.
(* pI2S est bijectif *)
Lemma pI2SK n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
{in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1), (S2pI i) \o (pI2S i) =1 id}.
(* L'image de S2pI (k décroit) *)
Lemma subset_S2pI n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
[set S2pI i p | p in 'N[n.+2, k.+1]]
\subset setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1).
(* L'image de p2SI (k croit) *)
Lemma subset_pI2S n k (i : 'I_n.+2) :
k.*2 = i -> i <= n ->
[set pI2S i t | t in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1)]
\subset'N[n.+2, k.+1].
(* Cardinalité des permutations dont tous les cycles sont de longueur 2 *)
(* On fait la preuve par induction en enlevant deux cycles à la fois *)
Lemma card_is_node n : #|'N[n.+1.*2]| = \prod_(i < n.+1) i.*2.+1.
(* Cardinal des configurations *)
Lemma card_cvalid n : #|'N2[n.+1.*2]| = (\prod_(i < n.+1) i.*2.+1) ^ 2.
Fact card_cvalid6 : #|'N2[6]| = 15 ^ 2.
(******************************************************************************)
(* *)
(* NOMBRE DE CONFIGURATIONS A 1 CYCLE *)
(* *)
(******************************************************************************)
(* Promouvoir une fonction en une permutation *)
Definition perm_of n (f : {ffun 'I_n.+1 -> 'I_n.+1}) : 'S_n.+1 :=
odflt 1%g [pick p | f == (pval p)].
Lemma perm_ofE n (f: {ffun 'I_n.+1 -> _}) : injective f -> perm_of f =1 f.
Lemma oddI_pre n (i : 'I_n.+2) : ~~ odd n -> odd (i - 1)%R = ~~ odd i.
Lemma oddIS n (i : 'I_n.+2) : ~~ odd n -> odd (i + 1)%R = ~~ odd i.
(* Traduire une configuration en une permutation en utilisant la liste S2l *)
Definition c2p n (c : config n.+1.*2) :=
perm_of ([ffun n : 'I_ _ => nth 0%R (c2l c) n]).
(* Récupération de la première permutation de la configuration *)
Definition fun_permL n (p : 'S_n.+2) :=
[ffun i : 'I_n.+2 =>
let k := p^-1%g i in
if odd k then p (k - 1)%R else p (k + 1)%R].
Lemma fun_permLK n (p : 'S_n.+2) i :
~~ odd n -> fun_permL p (fun_permL p i) = i.
Lemma injective_permL n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permL p).
Lemma fun_permLF n (p : 'S_n.+2) i : ~~ odd n -> fun_permL p i != i.
(* Récupération de la deuxième permutation de la configuration *)
Definition fun_permR n (p : 'S_n.+2) :=
[ffun i : 'I_n.+2 =>
let k := p^-1%g i in
if odd k then p (k + 1)%R else p (k - 1)%R].
Lemma fun_permRK n (p : 'S_n.+2) i :
~~ odd n -> fun_permR p (fun_permR p i) = i.
Lemma injective_permR n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permR p).
Lemma fun_permRF n (p : 'S_n.+2) i : ~~ odd n -> fun_permR p i != i.
(* Traduire une permutation telle que p 0 = 0 en une configuration *)
Definition p2c n (p: 'S_n.+2) : config n.+2 :=
(perm_of (fun_permL p), perm_of (fun_permR p)).
(* Permutation qui valent 0 en 0 *)
Definition perm_fix0 n : pred 'S_n.+1 := perm_on [set~ ord0].
Notation " 'F[ n ] " := (@perm_fix0 n).
Lemma perm_fix0P n p : p \in @perm_fix0 n = (p 0%R == 0%R).
Lemma c2l_codom n (p: 'S_n.+1.*2) : p 0%R = 0%R -> c2l (p2c p) = codom p.
Lemma card_perm_fix0 n : #|'F[n]| = n`!.
Lemma imp2c n: [set p2c p | p in 'F[n.*2.+1]] \subset 'N2[(n.+1).*2] :&: 'O[n].
Lemma imc2p n: [set c2p c | c in 'N2[(n.+1).*2] :&: 'O[n]] \subset 'F[n.*2.+1].
Lemma p2SK n : {in 'F[n.*2.+1], (@c2p _) \o (@p2c n.*2) =1 id}.
Lemma I_preE n (i: 'I_n.+2) : 0 < i -> (i - 1)%R = i.-1 :> nat.
Lemma c2lLE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.1) :
((forall i, p (p i) = i) ->
p (c2l c)`_i = (c2l c)`_(if odd i then (i - 1) else (i + 1)))%R.
Lemma c2lRE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.2) :
((forall i, p (p i) = i) -> (forall i, p i != i) -> uniq (c2l c) ->
p (c2l c)`_i = (c2l c)`_(if odd i then (i + 1) else (i - 1)))%R.
Lemma S2pK n : {in 'N2[n.+1.*2] :&: 'O[n], (@p2c n.*2) \o (@c2p _) =1 id}.
Lemma card_N2O n : #|'N2[n.+1.*2] :&: 'O[n]| = n.*2.+1 `!.
(******************************************************************************)
(* *)
(* PROBABILITÉ *)
(* *)
(******************************************************************************)
Open Scope ring_scope.
(* Le rapport entre tous les configurations de noeuds avec un cycle et toutes *)
(* les configurations *)
Definition Proba n : rat := #|'N2[n.+1.*2] :&: 'O[n]|%:R / #|'N2[n.+1.*2]|%:R.
Lemma ProbaE n : Proba n = n.*2.+1 `!%:R / ((\prod_(i < n.+1) i.*2.+1) ^2)%:R.
Lemma result : Proba 2 = 8%:R / 15%:R.
End Corde.
This page has been generated by coqdoc