proposition: Lemma sternD_sum_quo a b a' b' n : ((sternD_sum a b n) %:Q / (sternD_sum a' b' n) %:Q) %R = ((a +b)%N%:Q / ((a'+b')%N%:Q))%R .
proof: Proof. rewrite !sternD_sumE !ratN_M - mulf_div divff ?mul1r // intr_eq0. by move:(expn_eq0 3 n);case: ((3 ^ n)%N). 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)