proposition: Lemma normal_ofs_from_exten f g : f =1o g -> normal_ofs f -> normal_ofs g.
proof: Proof. move => h [sa sb]. split => //. move => x y xy; move: (xy)=> [[ox oy _]_]. by rewrite - h // - h //; apply: sa. move => x lx; move: (proj31 lx) => ox. rewrite -(h x ox) (sb _ lx). by apply: ord_sup_2funI => t /(Os_ordinal ox); apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)