proposition: Lemma normal_ofs_compose f g: normal_ofs f -> normal_ofs g -> normal_ofs (f \o g).
proof: Proof. move => /(normal_ofs_equiv2 OS0) pa /(normal_ofs_equiv2 OS0) pb. have h := ole0x (ofs_sincru (proj1 pb) (oleR OS0)). by move:(normal_ofs_compose1 OS0 OS0 h pa pb) => /normal_ofs_equiv1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)