proposition: Lemma Sn_neg x (T:= fun x => (- x)^-1): 0 < x -> Sn (T (Sn x)) = T x.
proof: Proof. move => xp; rewrite /T; congr (_ ^-1). rewrite invrN (opprK (Sn x)^-1) /Sn invrK opprB. set W := (floorq x)%:~R; set t := (1 + W * 2%N%:~R); set a := (1 + (W + W)). have ->: -t = (- (1 + (floorq x) * 2%N))%:Q. rewrite /t /W opprD opprD intrD - intrM - mulrNz //=. rewrite floor_sum intrD intr_N intrD intrM /t !doubleq -/W (addrACA W). by rewrite -/a addrA [1 + _]addrA [X in X + a - x]addrA subrK subrr add0r. 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)