proposition: Lemma GAr_Sbn B m n: GAr B.+1 m n = GAr B m n + (GAr B (m - fib (B.+2)) (n- fib(B.+3))) * (fib(B.+3) <= n) * (fib(B.+2) <= m).
proof: Proof. set b := (@ord_max B.+1). case: (ltnP n (fib B.+3)). rewrite muln0 addn0 => le1. have ha: (m < fib B.+2) || (n < fib B.+3) by rewrite le1 orbT. by rewrite -(GAr_big0 ha (leqnSn B)). case: (ltnP m (fib B.+2)). rewrite muln0 addn0 => le1 le2. have ha: (m < fib B.+2) || (n < fib B.+3) by rewrite le1. by rewrite -(GAr_big0 ha (leqnSn B)). rewrite !muln1 addnC /GAr => leqfm leqfn. set E := [set t | _]. have hb: forall (p: (pred {set 'I_B.+2})), #|[pred x | x \in p & x \in E]| = #|[set t | (p t) && ((Zeck_svalp t == m) && (Zeck_sval t == n)) ]|. by move => p; rewrite cardsE;apply: eq_card => x; rewrite !inE. set p := [pred t:{set 'I_B.+2} | b \in t]. have ha: #|[predI E & p]| = #|[pred x | (mem p) x & (mem E) x]|. by apply: eq_card => x; exact: andbC. move:(GARr_aux (leqnSn B)); set g := (fun t: _ => _); move => [ig aux]. have ig2: forall (t : {set 'I_B.+1}), Zeck_sval t = Zeck_sval (g t). move => t; rewrite/Zeck_sval; apply: (aux t (fun i => fib i.+2)). have ig2': forall (t : {set 'I_B.+1}), Zeck_svalp t = Zeck_svalp (g t). move => t; rewrite/Zeck_sval; apply: (aux t (fun i => fib i.+1)). have gpn: forall x, b \notin (g x). move => x; apply/imsetP => [[w _ eq2]]; have hc:= (ltn_ord w). move:(inordK (leq_trans hc (leqnSn B.+1))); rewrite - eq2. by apply/eqP/negbT; apply:gtn_eqF. rewrite - (cardID p) ha hb hb; congr addn; symmetry;last first. set pn := [pred t : {set 'I_B.+1} |(Zeck_svalp t == m) && (Zeck_sval t == n)]. rewrite cardsE -(card_imset pn ig). apply: eq_card => e; rewrite inE; apply/imsetP/idP. move => [x]; rewrite inE ig2 ig2' => ww ->;rewrite ww andbT; apply: gpn. move/andP => [hc hd]. have Hd: forall i, i \in e -> i <= B. move => i ie; have:= (ltn_ord i); rewrite ltnS leq_eqVlt; case/orP => // eb. have he: i = b by apply: ord_inj; rewrite (eqP eb) //. by move: hc; rewrite /p he !inE - he ie. set l :=(seq_to_seto B (seto_to_seq e)). suff ww : e = g l by exists l => //; rewrite /pn inE ig2 ig2' - ww. rewrite /l /g /seq_to_seto/seto_to_seq - map_comp /comp. apply/setP =>i; apply/idP/imsetP. move => ie; move:(inordK (Hd _ ie)) => sa. rewrite - mem_enum in ie; exists (inord i); last by rewrite sa inord_val. by apply /imsetP; exists (inord i) => //;rewrite (map_f _ ie). move => [j /imsetP [k /mapP [x]]];rewrite mem_enum => H. by move => -> -> -> /=; rewrite inordK ? inord_val // ltnS Hd. set pn := [pred t : {set 'I_B.+1} | Zeck_svalp t == m - fib B.+2 & Zeck_sval t == n- fib B.+3]. pose g1 t := b |: g t. have hc: forall t, p (g1 t) by move => t; apply/setU11. have ig1: injective g1. move => t1 t2; rewrite /g1 => w; apply: ig. by rewrite - (setU1K (gpn t1)) w (setU1K (gpn t2)). rewrite cardsE -(card_imset pn ig1). have ig3: forall t, fib B.+3 + Zeck_sval t = Zeck_sval (g1 t). by move => t; rewrite ig2 / Zeck_sval /g1 big_setU1. have ig3': forall t, fib B.+2 + Zeck_svalp t = Zeck_svalp (g1 t). by move => t; rewrite ig2' /Zeck_svalp /g1 big_setU1. apply: eq_card => e; rewrite inE; apply/imsetP/idP. move => [x]; rewrite inE; move => /andP[/eqP sa1 /eqP sa2] sb. rewrite sb hc - (subnK leqfn)- (subnK leqfm) - sa1 - sa2 addnC ig3'. by rewrite addnC ig3 !eqxx. move/and3P => [hc1 /eqP hd2 /eqP hd2']. set e1 := e :\ b. have Hd: forall i, i \in e1 -> i <= B. move => i /setD1P[ib ie]. have:= (ltn_ord i); rewrite ltnS leq_eqVlt; case/orP => // eb. by case/negP:ib; apply/eqP /ord_inj; rewrite (eqP eb). set l :=(seq_to_seto B (seto_to_seq e1)). suff ww : e = g1 l. exists l => //; rewrite /pn inE. by move: ww; rewrite -hd2 - hd2' => ->; rewrite -ig3 - ig3' !addKn !eqxx. rewrite /l /g1 /seq_to_seto/seto_to_seq - map_comp /comp. rewrite - {1} (setD1K hc1); congr setU. apply/setP =>i; apply/idP/imsetP. move => ie; move:(inordK (Hd _ ie)) => sa. rewrite - mem_enum in ie; exists (inord i); last by rewrite sa inord_val. by apply /imsetP; exists (inord i) => //;rewrite (map_f _ ie). move => [j /imsetP [k /mapP [x]]];rewrite mem_enum => H. by move => -> -> -> /=; rewrite inordK ? inord_val // ltnS Hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)