proposition: Lemma convergent_rat0 f: convergent_rat f 0 = f 0%N.
proof: Proof. rewrite /convergent_rat /convergent_num /convergent_den /=. by rewrite mulr1 mulr0 addr0 add0r divr1. 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)