proposition: Lemma oprod_increasing2 r f g: worder r -> substrate r = domain f -> substrate r = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) -> finite_set (substrate r) -> (oprod r f) <=o (oprod r g).
proof: Proof. move=> wor sf sg alo fse. apply/ordinal_le_P0; apply /order_le_compatible1. apply: orprod_wor => //; [ saw | hnf; aw ]. move=> i idf; rewrite ! LgV//; move: (alo _ idf) => [aa bb _]; fprops. apply: orprod_wor => //; [saw | hnf;aw ]. rewrite - sg sf; move=> i idf. have idg: inc i (domain g) by rewrite - sg sf. rewrite !LgV//; move: (alo _ idf) => [aa bb _]; fprops. rewrite /Lgcomp - sg sf. apply: oprod_increasing1. split => //; hnf; aw; trivial => i idf; rewrite LgV//;move: (alo _ idf) =>[aa bb _];fprops. split => //; hnf; aw; trivial. move => i idf; rewrite LgV//; move: (alo _ idf) =>[aa bb _]; fprops. aw => x xdf; move: (alo _ xdf) =>[aa bb le]. apply /order_le_compatible1; rewrite !LgV//; fprops. by rewrite (ordinal_o_o aa) (ordinal_o_o bb); apply/ordinal_le_P0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)