proposition: Lemma nds_sol_fix_pt (f := nds_sol): [/\ f \0c = \1c, f \1c = \1c & nds_fixpt_eq f].
proof: Proof. apply/ nds_max_bd_prop. move:nds_sol_v => H. split. - by rewrite /f /nds_sol; Ytac0. - by rewrite - nat_to_B1 /f- (H 1) Nds.nds_sol1. - move => n k nN n2 kp kn. have kv:= (B_to_nat_pa (NS_lt_nat kn nN)). have nv :=(B_to_nat_pa nN). move: n2 kp kn; rewrite -kv -nv;set K := (B_to_nat k); set N := (B_to_nat n). rewrite - nat_to_B2. move => /nat_to_B_le ln1 /nat_to_B_pos kp /nat_to_B_lt lkn. have l0kn: 0 < K < N by rewrite kp lkn. rewrite /f - H - nat_to_B_diff - H - ndsC_v - nat_to_B_prod. apply/nat_to_B_le; exact: (Nds.nds_sol_bd ln1 l0kn). move => n nN n2. move:(B_to_nat_pa nN); set N := (B_to_nat n) => nv. move: n2; rewrite - nat_to_B2 - nv => /nat_to_B_le ln1. move:(Nds.nds_sol_max ln1) => [k /andP [/nat_to_B_pos kp /nat_to_B_lt lkn] eq]. exists (nat_to_B k); split => //. by rewrite - nat_to_B_diff / f -H -H -ndsC_v -nat_to_B_prod - eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)