proposition: Lemma Stern_prev_fctK: cancel Stern_prev_fct Sn.
proof: Proof. move => x; rewrite /Stern_prev_fct /Sn; set y := floorq (- x)^-1. rewrite - intrM - intrM -[((- x)^-1 - 1 - (y * 2)%:~R)] addrA. rewrite - (opprD 1) -!(intrD _ 1%:Z) -{1} intr_N. rewrite floor_sum opprD (addrCA (floorq _)) - (opprB _ y) !mulz2 addrK. have -> : (1 + (- (1) - y + (- (1) - y))) = (- (1 + y + y)). by rewrite !addrA addrN add0r - !opprD (addrC y). by rewrite (addrA 1 y) opprB intr_N addKr invrN opprK invrK. 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)