proposition: Lemma fib_sum_bound a b n: a <= fib n.+1 -> b <= fib n -> a + b = fib n.+2 -> (a = fib n.+1) /\ (b = fib n).
proof: Proof. move => sa sb /esym /eqP; rewrite fibSS -(subnK sa) -(subnK sb) addnACA. by rewrite -{2}(add0n (a+b)) eqn_add2r addn_eq0 => /andP [] /eqP -> /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)