proposition: Lemma all_der_p13_ter f b (g:= all_der f b): normal_ofs f -> all_der_bound f b -> f \0o = \0o -> f \1o <> \1o -> normal_ofs (g \1o).
proof: Proof. move => ha hb hc hd; apply:(all_der_p13_bis) => //; fprops. by move => x /olt1 ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)