proposition: Lemma lucas_plus_lucas a b c: b <= c -> (lucas a == lucas b + lucas c) = [ || [&& a==3, b==0 & c==0], [&& a==0, b==1 & c==1] | (c==b.+1) && (a==b.+2)].
proof: Proof. have Ha i: i != 1 -> 2 <= lucas i. by case: i => [| [| i _]]//; apply: ltnW; apply: (@lucas_monotone 2 i.+2). have Hb i: 2 <=i -> 3 <= lucas i by apply:(lucas_monotone (m:=2)). case az: (a== 0). rewrite (eqP az) !andbF /= orbF => lbc; case: (ltngtP 1 b) => b1. + apply/negP => /eqP h. by move: (Hb _ b1); rewrite -(ltn_add2r (lucas c)) - h. + move: b1; rewrite ltnS leqn0 => /eqP ->. by rewrite -{1} (addn0 (lucas 0)) eqn_add2l /= (ltn_eqF (lucas_gt0 c)). + by rewrite - b1 /= -[lucas 0]/(1+(lucas 1)) eqn_add2l lucas_injective_bis. case bz: (b == 0). rewrite (eqP bz) /= => _. case cz: (c== 0). rewrite (eqP cz) /= andbT orbF; exact: (lucas_injective_bis a 3). case co: (c== 1). rewrite (eqP co) andbF /=; exact: (lucas_injective_bis a 2). rewrite andbF /=; apply/negP => /eqP h. case:(ltnP c a) => ha; last first. have /lucas_monotone: 0 < a <=c by rewrite ha lt0n az. by rewrite h ltnNge leqnSn. have /lucas_monotone ww : 0 < c.+1 <= a by rewrite ha. have /prednK cp : O < c by rewrite lt0n cz. move: ww; rewrite h -{1}cp lucasSS addnC cp leq_add2r lucas_monotoneE. rewrite !andbF /= -!(eqSS c.-1) cp co /= andbT orbF => c2. move: h; rewrite (eqP c2); clear;case: a => [|[|[|[| a]]]] // ea. have /lucas_monotone :0 < 4 <= a.+4 by []. by rewrite ea. rewrite /= andbF /=. rewrite leq_eqVlt; case/orP => ebc. rewrite - (eqP ebc) (ltn_eqF (ltnSn b)) /=; apply/negP => /eqP h. case: (ltngtP b.+1 a) => lab. + have /lucas_smonotone ha: 0 < b < b.+1 by rewrite ltnSn lt0n bz. have /lucas_monotone: 0 < b.+2 <= a by rewrite lab. by rewrite lucasSS h leq_add2r leqNgt ha. + have /lucas_monotone: 0 < a <= b by rewrite lt0n - ltnS lab az. by rewrite h -{3} (add0n (lucas b)) leq_add2r leqNgt lucas_gt0. + move /eqP:h; rewrite -lab. move:bz; clear; case: b => // b _. by rewrite lucasSS eqn_add2l lucas_injective_bis; apply/negP /eqP. apply/eqP/andP; last by move => [/eqP -> /eqP ->]; rewrite lucasSS addnC. move => h. have c1:= (ltn_predK ebc). have /lucas_monotone: 0 < b <= c.-1 by rewrite lt0n bz - ltnS c1 ebc. rewrite - (leq_add2r (lucas c)) -h addnC - {1} c1 -lucasSS c1 => lb. case: (ltngtP a c.+1) => la. + have /lucas_monotone: 0 < a <= c by rewrite lt0n az -ltnS la. by rewrite h -{2}(add0n (lucas c)) leq_add2r leqNgt lucas_gt0. + have /lucas_smonotone: 0 < c.+1 < a by rewrite la. by rewrite ltnNge lb. + move /eqP: h; rewrite la - c1 lucasSS addnC eqn_add2r lucas_injective_bis. by move/eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)