proposition: Lemma orsum2_gleP x x': gle (order_sum2 r r') x x' <-> [/\ inc x (canonical_du2 (substrate r) (substrate r')), inc x' (canonical_du2 (substrate r) (substrate r')) & [\/ [/\ Q x = C0, Q x' = C0 & gle r (P x) (P x')], [/\ Q x <> C0, Q x' <> C0 & gle r' (P x) (P x')] | (Q x = C0 /\ Q x' <> C0)]].
proof: Proof. have Ha: C1 <> C0 by fprops. set S1:= (canonical_du2 (substrate r) (substrate r')). have S1p: S1 = (sum_of_substrates (variantLc r r')). by rewrite /sum_of_substrates canonical2_substrate. split. move /orsum_gleP; rewrite - S1p. move=> [xs xns' osr]; split => //; move: osr => [] []. move /cdo_gleP => aux nsQ;case: aux. by move=> [e1 e2]; rewrite e1 e2 in nsQ;case: nsQ. case; first by move=> e1 e2; rewrite e1 e2 in nsQ; case: nsQ. move=> [e1 e2]; constructor 3; rewrite e2; split => //. move=> <-. case: (candu2_pr2 xs) => ->; aw; [constructor 1| constructor 2]; split => //. move=> [xs1 x's1 etc]; apply/orsum_gleP; split => //; try ue. case: etc. move=> [qxa qx'a lrxx']; right; rewrite qxa qx'a; aw;split => //. move=> [qxa qx'a lrxx']; right. have ->: (Q x' = C1) by case: (candu2_pr2 x's1) => //. have ->: (Q x = C1) by case: (candu2_pr2 xs1) => //. aw; split => //. move=> [qxa qx'a]; left; rewrite qxa. have ->: Q x' = C1 by case: (candu2_pr2 x's1) => //. apply: cdo_glt1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)