proposition: Lemma OTsum_Mle0 a b: order_type a -> order_type b -> a <=t a+t b /\ b <=t a +t b.
proof: Proof. move => oa ob. move: cdo_wor => [wor sr]. have ha: substrate canonical_doubleton_order = domain (variantLc a b). by rewrite sr; aw. have hb: sub (singleton C0) (domain (variantLc a b)). aw => t /set1_P->; apply: set2_1. have hc: sub (singleton C1) (domain (variantLc a b)). aw => t /set1_P->; apply: set2_2. have hd: order_type_fam (variantLc a b). by hnf; aw => x xt; try_lvariant xt. move:(OT_sum_increasing4 (proj1 wor) ha hb hd). move:(OT_sum_increasing4 (proj1 wor) ha hc hd). rewrite - OT_sum2_pr. have ta1: domain (restr (variantLc a b) (singleton C1)) = singleton C1 by aw. have ta0: domain (restr (variantLc a b) (singleton C0)) = singleton C0 by aw. have td0: Vg (restr (variantLc a b) (singleton C0)) C0 = a. by rewrite LgV//; aww. have td1: Vg (restr (variantLc a b) (singleton C1)) C1 = b. by rewrite LgV //; aww. rewrite - td0 in oa; rewrite - td1 in ob. move: hb hc; rewrite -ha => hb hc. move: (iorder_osr (proj1 wor) hb); rewrite {1} /order_on - {3} ta0 => tc0. move: (iorder_osr (proj1 wor) hc); rewrite {1} /order_on - {3} ta1 => tc1. by rewrite (OTsum_set1 tc1 ta1 ob) (OTsum_set1 tc0 ta0 oa) td0 td1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)