proposition: Lemma all_der_prod_cor c: \2o <=o c -> normal_ofs (fun i => c ^o (oopow i)).
proof: Proof. move => cp. move: (ord2_trichotomy1 cp) => [sa sb]. have oc:=proj32 cp. have sc: c *o \0o = \0o by rewrite oprod0r. have sd: c *o \1o <> \1o by rewrite (oprod1r oc). have se:= (olt_leT olt_02 cp). have os1:= OS1. move: (all_der_prod_aux se)=> [ha hb]. move:(all_der_p13_ter ha hb sc sd). apply:normal_ofs_from_exten => x ox; rewrite all_der_prod // oprod1r;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)