proposition: Lemma Fib_sub n m: natp n -> natp m -> m <=c n-> Fib (n -c m) = Yo (evenp m) (Fib n *c Fib (csucc m) -c Fib (csucc n) *c Fib m) (Fib (csucc n) *c Fib m -c Fib n *c Fib (csucc m)).
proof: Proof. move: even_zero => ez. move => nN; move: n nN m; apply: Nat_induction. move=> m mN /cle0 ->; rewrite (Y_true ez) Fib0 cprod0r cprod0l. by rewrite cdiff_nn Fib0. move => n nN Hrec m mN; case: (equal_or_not m \0c) => mz. move:(NS_succ nN) => ha; move:(NS_Fib ha) => hb. rewrite mz (Y_true ez) succ_zero Fib0 Fib1 cprod0r. by rewrite (cdiff_n0 ha) (cprod1r (CS_nat hb)) (cdiff_n0 hb). move:(cpred_pr mN mz); set c := cpred m; move => [cN cv]. rewrite cv (cdiff_pr6 nN cN); move /(cleSSP (CS_nat cN) (CS_nat nN)) => h. move: (NS_Fib cN)(NS_Fib nN)(NS_Fib (NS_succ cN))(NS_Fib (NS_succ nN)). move => qa qb qc qd. rewrite (Hrec _ cN h) (Fib_rec cN) (Fib_rec nN) cprodDr cprodDl. Ytac ec; first rewrite (Y_false (proj2 (succ_of_even ec))) cdiff_pr5; fprops. rewrite (Y_true (succ_of_odd (conj cN ec))) cdiff_pr5; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)