proposition: Lemma psi_sint_phi n : (psi `[n]).*2 = (phi n.+1).-1.
proof: Proof. have [|nP] := leqP n 0; first by case: (n)=> //; rewrite psi_sint0. apply/eqP; rewrite -(eqr_nat (Num.NumDomain.clone _ int)). rewrite -muln2 natrM mulr_natr. rewrite psi_aux_sint // psi_auxE_lt. rewrite (_ : [fset _ in _ | _] = [fset i in `[n] | delta (troot n) <= i]); last first. apply/fsetP=> i; rewrite !inE; congr (_ && _). by rewrite prednK ?troot_gt0 // root_delta_le. rewrite sint_sub ?delta_gt0 ?troot_gt0 // card_sint //. rewrite (_ : \sum_(i <- _ | _) _ = phi (delta (troot n))); last first. rewrite phiE. rewrite [RHS](eq_bigl (fun i : 'I_ _ => (i : nat) \in (enum_fset `[n]))); last first. move=> i. by rewrite mem_sint leq0n (leq_trans (ltn_ord _)) // delta_root_le. elim: enum_fset (fset_uniq `[n]) => /= [_|a l IH /andP[aNIl lU]]. by rewrite big_nil big1. rewrite big_cons /= IH //; case: leqP => aLb; last first. rewrite prednK ?troot_gt0 // in aLb. apply: eq_bigl => i; rewrite inE eqn_leq [a <= i]leqNgt. by rewrite (leq_trans (ltn_ord i)) ?andbF // -root_delta_le. have aLn : a < Δ(∇n). by rewrite -root_delta_lt -[troot n]prednK // troot_gt0. rewrite [RHS](bigD1 (Ordinal aLn)) ?(inE, eqxx) //=. congr ((_ + _)%nat). apply: eq_bigl => i; rewrite inE -val_eqE /=. by case: (_ =P _); rewrite ?andbT // => ->; rewrite (negPf aNIl). set m := troot n. rewrite -[n - _]/(tmod n). set p := tmod n. rewrite phi_deltaE. rewrite -{2}[m]prednK ?troot_gt0 //. rewrite mulSn addnCA [(2 ^ _ + _)%nat]addnC addnK add1n. rewrite addnS -addSn prednK; last first. by rewrite muln_gt0 expn_gt0. rewrite -{3}[m]prednK ?troot_gt0 //. rewrite expnS mul2n -addnn mulnDr addnA natrD addrK. rewrite mulnC -mulnDl addSnnS prednK ?troot_gt0 //. rewrite -mulr_natr -natrM muln2 eqr_nat. rewrite phi_modSE -/m -/p. rewrite add1n -pred_Sn addnC -{4}[m]prednK ?troot_gt0 //. by rewrite expnS mulnCA mul2n. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)