proposition: Lemma nontrivial_rev_ring : nontrivial_ring m (rev_ring r).
proof: Proof. have [[[ntFr ntFCr] rN] rF] := (andP nt_r, diskN_rev_ring r_ok, fband_rev_ring). apply/andP; split; [congr (_ <= _): ntFCr | congr (_ <= _): ntFr]. by apply: eq_n_comp_r => x; rewrite !inE /= rN rF. by apply: eq_n_comp_r => x; rewrite !inE /= rN -rF negbK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry patch sew snip color chromogram) fourcolor(coloring kempe)