proposition: Lemma Exercise4_8o x (comp:= fun X => X -s1 (the_least r)): inc x (substrate r) -> inc (char_fun (comp (E47S r x)) E48P) E48API.
proof: Proof. move: (Exercise4_7e) => s1 xsr. 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 => /setC1_P [] /Zo_hi [_ jx] njl /Zo_P []/Zo_P [pa pb]/set1_P nil. apply /setC1_P;split => //; apply /Zo_P;split => //; split => //. move: lr => [or _];order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)