proposition: Lemma union2_wor r A B C: total_order r -> sub A (substrate r) -> sub B (substrate r) -> sub C (A \cup B) -> worder (induced_order r A) ->worder (induced_order r B) -> worder (induced_order r C).
proof: Proof. move => [or tor] Asr Bsr cab [or1 wo1] [or2 wo2]. have cs: sub C (substrate r). by move => t tc;move:(cab _ tc);case /setU2_P => h; [apply: Asr| apply: Bsr]. move:(iorder_osr or Asr)(iorder_osr or Bsr)(iorder_osr or cs). move=>[oA sA][oB sB][oC sC]. split => //; rewrite sC => X XC neX. rewrite sA in wo1; rewrite sB in wo2. have Xp: (X \cap A) \cup (X \cap B) = X. by rewrite - (set_IU2r X A B); apply/ setI2id_Pl; apply: (sub_trans XC cab). rewrite (iorder_trans _ XC). case: (emptyset_dichot (X \cap A)) => ne1. have XB: sub X B by rewrite -Xp ne1 set0_U2; apply:setI2_2. by move:(wo2 _ XB neX); rewrite (iorder_trans _ XB). case: (emptyset_dichot (X \cap B)) => ne2. have XA: sub X A by rewrite -Xp ne2 setU2_0; apply:setI2_2. by move:(wo1 _ XA neX); rewrite (iorder_trans _ XA). have pc: sub (X \cap A) A by apply: subsetI2r. have pd: sub (X \cap B) B by apply: subsetI2r. move: (wo1 _ pc ne1)(wo2 _ pd ne2). rewrite (iorder_trans _ pc) (iorder_trans _ pd). move: (sub_trans XC cs) => qa. move: (sub_trans pc Asr) => qb. move: (sub_trans pd Bsr) => qc. move => [a ap][b bp]; move: ap bp; rewrite /least ! iorder_sr//. move => [] /setI2_P [aX aA] al [] /setI2_P [bX bB] bl. have [c [cX ca cb]]: exists c, [/\ inc c X, gle r c a & gle r c b]. case: (tor _ _ (Asr _ aA)(Bsr _ bB)) => aux. exists a; split => //; order_tac; exact (Asr _ aA). exists b; split => //; order_tac; exact (Bsr _ bB). exists c;split => //; rewrite iorder_sr//; move => x xX; apply /iorder_gle0P => //. move: xX; rewrite - Xp => /setU2_P; case => h. move: (al _ h) => h1; move: (iorder_gle1 h1) => h2; order_tac. move: (bl _ h) => h1; move: (iorder_gle1 h1) => h2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)