proposition: Lemma at_most_regionsP n m : plain_map m /\ at_most_regions n m <-> exists g, eq_map m (fin_color_map n g).
proof: Proof. have RleqP i j : reflect (i%:R <= j%:R)%Rval (i <= j) := @intR_leP R i j. elim: n m => [|n IHn] m; do [split=> [[mP [f fP]] | [g gP]]; last first]. - by split; [split=> t | exists (fun=> 'z_0)] => z /gP[]. - by exists (fun=> 0%Rval) => z t; split=> [/(map_cover mP)[/fP[i /ltP]] | []]. - have mP: plain_map m. split=> z t /gP[i lti [Dgz Di]]; first by apply/gP; exists i; rewrite ?Dgz. by move=> u /gP[_ _ [Dgu _]]; apply/gP; exists i; rewrite -?Dgu. have [_ [|_ [f fP]]] := IHn (fin_color_map n g); first by exists g. have [zn znP]: (exists zn, forall z, g z == n%:R -> g zn == n%:R)%Rval. have [[zn]|] := Rclassic (exists z, g z == n%:R)%Rval; first by exists zn. by move=> g'n; exists 'z_0 => z gz_n; case: g'n; exists z. split=> //; exists [eta f with n |-> zn] => z /gP[i]; rewrite ltnS leq_eqVlt. case/predU1P=> [-> | lt_i_n] /= [_ Dgz]. by exists n; [apply/ltP | apply/gP; exists n; rewrite // eqxx Dgz (znP z)]. have [|j /ltP-lt_j_n [i1 _ [Dfj Di1]]] := fP z; first by exists i. by exists j; [apply/ltP/leqW | apply/gP; exists i; rewrite ?ltn_eqF ?leqW]. have [[|g gP _]] := IHn [map z t | m z t /\ ~ m z (f n)]. split; first split=> z t [/(map_sym mP)mtz m'zn] => [|u [mtu m'tn]]. - by rewrite (map_transl mP mtz (f n)). - by rewrite -(map_transl mP mtz). exists f => z [/fP[i /ltP-le_i_n m_iz] m'zn]. exists i; [apply/ltP | by split=> // /(map_transl mP m_iz)]. by rewrite ltn_neqAle; case: eqP m'zn => // <- []; apply/(map_sym mP). pose h z := (IF m z (f n) then n%:R else IF m z z then g z else n.+1%:R)%Rval. exists h => z t; split=> [mzt | [i le_i_n [Dhz Dht]]]. have [m_z m_t] := map_cover mP mzt. have [mzn | m'zn] := Rclassic (m z (f n)). by exists n; rewrite // /h !IFR_then // -(map_transl mP mzt). have [[//| i /leqW-lt_i_n1 Dgzt_i] _] := gP z t; exists i => //. by rewrite /h -(map_transl mP mzt) IFR_else 1?IFR_then // IFR_else ?IFR_then. generally have m_t, m_z: z Dhz / m z z; last have {}m_t: m t t by apply: m_t. have: (h z < n.+1%:R)%Rval by rewrite Dhz Dht; apply/RleqP; rewrite -ltnNge. by apply: RcontraR => m'z; rewrite /h !IFR_else // => /(map_cover mP)[]. generally have m_tnP, m_zn: z Dhz m_z / m z (f n) <-> i == n. split=> [m_zn | /eqP-Di]. by rewrite eqn_leq -ltnS le_i_n; apply/RleqP; rewrite -Dht -Dhz /h IFR_then. have: ~ (h z < n%:R)%Rval by case; rewrite Dhz Dht Di. apply: RcontraR => m'zn; rewrite /h IFR_else // IFR_then //. have [[//|j lt_j_n [_ Dj]] _] := gP z z; rewrite {}Dj. by apply/RleqP; rewrite -ltnNge. have /orP[Di | lt_i_n]: (i == n) || (i < n) by rewrite -leq_eqVlt. by rewrite (map_transr mP (_ : m t (f n))) (m_zn, m_tnP). have [_ [|//]] := gP z t; exists i => //; move: (Dhz) Dht. by rewrite /h !m_tnP ?ltn_eqF //; do 2!rewrite IFR_else // IFR_then //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path ssralg ssrint) fourcolor(real realplane realsyntax realprop) fourcolor(grid approx)