proposition: Lemma all_der_p12 i : ordinalp i -> f \0o = \0o -> g \0o i = \0o.
proof: Proof. move => oi f0. move: i oi; apply least_ordinal2 => y oy etc. case: (ozero_dichot oy) => yz; first by rewrite yz all_der_p2 //; fprops. move: (all_der_p8 OS0 yz etc)=> [x ox h]. case (ozero_dichot ox) => xz; first by rewrite - {1} xz. by move: (all_der_p5 oy xz); rewrite - h; move /olt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)