proposition: Lemma fib_plus_fib a b c: b <= c -> (fib a == fib b + fib c) = [ || (b == 0) && (fib a == fib c), [&& b ==c, (c==1) || (c== 2) & a==3], [&& b ==1, c==3 & a==4] | (c==b.+1) && (a==b.+2)].
proof: Proof. case:b. move => _. case wa: ((c == 1) && (a == 2)); first by move/andP:wa => [/eqP -> /eqP ->]. by case wb: (0==c); rewrite - ? (eqP wb) /= orbF. move => b; rewrite/= !eqSS;case:b. rewrite add1n - (addn1 (fib c)) (eq_sym 1 c) /=. case: c => // c _; rewrite !eqSS. case cz: (c==0); first by rewrite (eqP cz) (fib_eq a 3) /= !andbF !orbF. case co: (c==1); first by rewrite (eqP co) (fib_eq a 3) /= !andbF !orbF. case ct: (c==2); first by rewrite (eqP ct) (fib_eq a 4) /= ! andbF!orbF. simpl; apply/negP => /eqP ha. case: (ltnP c.+1 a) => lac; last first. by move: (fib_monotone lac); rewrite ha addn1 ltnn. have w: (3 <= c) by rewrite ltn_neqAle eq_sym ct ltn_neqAle eq_sym co lt0n cz. move: (fib_monotone lac); rewrite ha fibSS leq_add2l => la. by move: (leq_trans (fib_monotone w) la). move => b; rewrite leq_eqVlt; case/orP => ha. have hh:=(ltn_eqF (ltnSn b)). rewrite - (eqP ha) !eqSS eqxx hh /= orbF. case bz: (b==0); first by rewrite (eqP bz) (fib_eq a 3) !andbF !orbF. simpl; apply/negP => hb. case: (ltngtP b.+3 a) => lac. + move: (fib_monotone lac); rewrite (eqP hb) fibSS leq_add2r. by apply/negP;rewrite -ltnNge fib_smonotone_bis. + rewrite ltnS in lac; move: (fib_monotone lac). by rewrite (eqP hb) leqNgt ltn_paddr // fib_gt0. + by move: hb; rewrite - lac fibSS eqn_add2l fib_eq // !eqSS bz hh /= andbF. rewrite (ltn_eqF ha) /=; move: ha; rewrite leq_eqVlt; case/orP=> ha. by rewrite - (eqP ha) addnC -fibSS eqxx fib_eq !eqSS !andbF!orbF. have cp:=(ltn_predK ha). rewrite (gtn_eqF ha) /=; apply/negP => hb. case: (ltngtP a c.+1) => lac. + rewrite ltnS in lac; move: (fib_monotone lac). by rewrite leqNgt (eqP hb) ltn_paddl // fib_gt0. + move:(fib_monotone lac); rewrite (eqP hb) fibSS leq_add2r leqNgt. by rewrite fib_smonotone // !ltnS (ltnW(ltnW ha)) andbT. + move: hb; rewrite lac -cp fibSS addnC eqn_add2r fib_eq !eqSS andbF orbF. rewrite -eqSS -(eqSS _ 1) !cp (gtn_eqF ha) /= => /andP [h1 h2]. by move: ha; rewrite (eqP h1) (eqP h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)