proposition: Lemma GAr_big0 A B m n: ((m < fib A.+2) || (n < fib A.+3)) -> A <= B -> GAr A m n = GAr B m n.
proof: Proof. rewrite /GRr => ns lenm. move:(GARr_aux lenm); set g := (fun t:_ => _); move => [Hb Hx]. move:lenm; rewrite - ltnS => lenm. have HB0 l i: i \in l -> fib (i.+1) <= Zeck_valp l. elim: l i => // [a l Hrec i /=]; rewrite in_cons Zeckvp_cons; case/orP. move /eqP => ->; case: a => // a; apply: leq_addr. move/Hrec/leq_trans => -> //; exact:leq_addl. pose Hw x := (inordK (leq_trans (ltn_ord x) lenm)). have Hc1: forall t, Zeck_sval t = Zeck_sval (g t). move => t; apply: (Hx t (fun z => (fib z.+2))). have Hc2: forall t, Zeck_svalp t = Zeck_svalp (g t). move => t; apply: (Hx t (fun z => (fib z.+1))). set pn := [pred t : {set 'I_A.+1} | Zeck_svalp t == m & Zeck_sval t == n]. rewrite /GAr cardsE -(card_imset pn Hb). apply: eq_card => e; rewrite inE; apply/imsetP/idP. by move => [x]; rewrite inE Hc1 Hc2 => ww ->. set l :=(seq_to_seto A (seto_to_seq e)) => eqa. move: (eqa) => /andP[/eqP eqb /eqP eqc]. suff ww : e = g l by exists l => //; rewrite /pn inE Hc1 Hc2 - ww. have Hd: forall i, i \in e -> i <= A. move => i ie. have ie': (nat_of_ord i) \in (seto_to_seq e). by rewrite /seto_to_seq map_f // mem_enum. move: (Zeckv_bnd0 ie')(HB0 _ _ ie'). rewrite Zeck_val_cv1 Zeck_valp_cv1 eqb eqc => la lb; case/orP: ns => lc. by move: (leq_ltn_trans lb lc) => /fib_monotone_bis; rewrite !ltnS. by move: (leq_ltn_trans la lc) => /fib_monotone_bis; rewrite !ltnS. 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. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)