proposition: Lemma fib_square: forall n, (fib n)^2 = if odd n then (fib n.+1 * fib n.-1).+1 else (fib n.+1 * fib n.-1).-1.
proof: Proof. case=> [|n] //; move: (fib_sub (n.+1) n (leqnSn _)). rewrite subSn // subnn fib1 -[in odd _.+1]add1n oddD addTb. case: odd=> H1; last first. by rewrite -[(_ * _).+1]addn1 [in _ + _]H1 addnC subnK // ltnW // -subn_gt0 -H1. by apply/eqP; rewrite -subn1 [in _ - _]H1 subKn // ltnW // -subn_gt0 -H1. Qed.
imports: mathcomp(all_ssreflect all_algebra)