proposition: Lemma convergent_rat1 f: f 1%N != 0 -> convergent_rat f 1 = SCF [:: f 0%N ; f 1%N].
proof: Proof. move => h. rewrite /convergent_rat /convergent_num /convergent_den /=. rewrite mulr1 mulr0 !addr0 add0r mulr1 mulrDl -mulrA mulrC mulrVK //. 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)