proposition: Lemma Exercise4_8n x: inc x (substrate r) -> inc (char_fun (E47S r x) (irreds r)) (substrate E48AJImo).
proof: Proof. have s1: sub (irreds r) (substrate r) by apply: Zo_S. move => xsr. move: (Exercise4_7q xsr) (Exercise4_7g xsr) => q0 q1. move: Exercise4_8m => [[p1 p2] p3]; rewrite p3. split; last by rewrite char_fun_V_a //. apply /(Exercise4_8iP s1); rewrite /char_fun; saw. apply: char_fun_f. move=> i j isr jsr ij; rewrite !LfV//; try apply: char_fun_axioms. rewrite /varianti. Ytac jE; last by move=> zo; case: card1_nz. move=> _; Ytac iE => //; case: iE. move: jE isr => /Zo_hi [_ jx] /Zo_P [pa pb]; apply /Zo_P;split => //. move: lr => [or _];split => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)