proposition: Lemma foo L x (n := size L): SCF (rcons L x) = (x * (convergent_num (nth 0 L) n.+1) + (convergent_num (nth 0 L) n)) / (x * (convergent_den (nth 0 L) n.+1) + (convergent_den (nth 0 L) n)).
proof: Proof. rewrite /n; clear n. elim /last_ind: L x. move => x. by rewrite /convergent_num /convergent_den /= mulr1 mulr0 add0r divr1. move => L a Hrec b. rewrite SCF_recl Hrec size_rcons convergent_num_rec convergent_den_rec. rewrite nth_rcons ltnn eqxx. set f1 := (nth 0 L); set f2 := (nth 0 (rcons L a)). admit. Abort. End ContinuedFractions. Definition fusc_prop f:= [/\ f 0 = 0, f 1 = 1, (forall n, f (n.*2) = f n) & (forall n, f (n.*2.+1) = f n + f (n.+1)) ]. Lemma fusc_ind P: P 0 -> P 1 -> (forall n, P n -> P (n.*2)) -> (forall n, P n -> P n.+1 -> P (n.*2.+1)) -> forall n, P n. Proof. move => h0 h1 he ho n. elim: n {-2} n (leqnn n) => [ []| n Hrec [|m]] //. rewrite ltnS -(odd_double_half m);case:(odd _). rewrite add1n - doubleS => /(leq_ltn_trans (double_le1 m./2)) h. by apply: he; apply: Hrec. case: (m./2) => // k /(leq_trans (double_le3 k)) h. by apply:ho; apply: Hrec => //; apply: ltnW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)