proposition: Lemma sincr_ofs_exten f1 f2: sincr_ofs f1 -> sincr_ofs f2 -> (forall x, ordinalp x -> exists2 y, ordinalp y & f1 x = f2 y) -> (forall x, ordinalp x -> exists2 y, ordinalp y & f2 x = f1 y) -> f1 =1o f2.
proof: Proof. move => i1 i2 rs1 rs2; apply: (least_ordinal2) => b ob pb. move: (rs1 _ ob) => [a oa av]; rewrite av. case (oleT_ell oa ob) => cab; first by rewrite cab. by move: (pb _ cab)(proj2 (i1 _ _ cab)); rewrite av. move: (rs2 _ ob) => [c oc cv];rewrite cv. case (oleT_ell oc ob)=> cbb;first by rewrite cbb. by move: (pb _ cbb) (proj2 (i2 _ _ cbb)); rewrite cv => ->. by move: (i2 _ _ cab) (i1 _ _ cbb); rewrite av cv; move => h1 [/(oltNge h1)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)