proposition: Lemma ord_pow_axioms: OIax3 \2o (fun z:Set => \1o) oprod2.
proof: Proof. move: (olt_12) (olt_02) => l12 l02. split; first split; first split. - move => a a2 /=; rewrite (oprod1l (proj32 a2)); exact: (olt_leT l12 a2). - move => a [_ a2 _] /=; rewrite (oprod1l a2); exact: (oleR a2). - move => a b a2 b2; apply:(oprod_Meq1lt (olt_leT l12 b2) (olt_leT l02 a2)). - by move => a b a' b' la lb; apply:oprod_Mlele. - move => _ _ _ _ /=;fprops. - move => a b [_ oa _] ab /=; rewrite !oprod1l //; exact: (proj32_1 ab). - by move => a [_ oa _] /=; rewrite oprod1l. - move => a ab; apply: normal_ofs_equiv2; fprops; apply: oprod_normal. exact:(olt_leT l02 ab). - by move => a b c [_ oa _] [_ ob _][_ oc _]; symmetry;apply:oprodA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)