proposition: Lemma Stern_succ_fctK: cancel Sn Stern_prev_fct.
proof: Proof. move => x;rewrite /Stern_prev_fct /Sn invrN invrK opprB - intrM. rewrite -{2}(intrD _ 1%:Z) -intr_N floor_sum - intrM - intr_N. rewrite -[in X in _ + X] mulNr (opprB (floorq x)). rewrite {2} mulz2 (addrA 1) addrK -(addrA x) -opprD (addrC _ 1) - !(intrD _ 1%:Z). by rewrite mulz2 mulz2 addrACA addrA addrNK. 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)