proposition: Lemma normal_ofs_equiv1 f: normal_ofs1 f \0o <-> normal_ofs f.
proof: Proof. apply:(iff_trans (normal_ofs_equiv f _)). split; move=> [h2 h3]; split => //. - move=> x y xy; apply: h2=> //; apply: ole0x. by move: xy=> [[ox _ _] _]. - move=> x [pa pb pc]. rewrite - {2} (ointv_pr1 pa). apply: h3 => //; apply /oltP0;split;fprops. - by move=> x y r1 r2; apply: h2. - move => x lx wnz. have [ox _ _] := lx. by rewrite (ointv_pr1 ox); apply: h3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)