proposition: Lemma isum_q8 u v: ordinalp u -> ordinalp v -> forall x y, gle (order_sum2 (ordinal_o u) (ordinal_o v)) x y <-> [/\ inc x (dsum u v), inc y (dsum u v) & [\/ [/\ Q x = C0, Q y = C0 & (P x) <=o (P y)], [/\ Q x <> C0, Q y <> C0 & (P x) <=o (P y)] | Q x = C0 /\ Q y <> C0]].
proof: Proof. move => ou ov x y. move: C0_ne_C1 C1_ne_C0 => nea neb. have aux z: inc z (dsum u v) -> ordinalp (P z). move/candu2P => /proj2; case => - [vv _]. by apply (Os_ordinal ou). by apply (Os_ordinal ov). apply: (iff_trans (orsum2_gleP (ordinal_o u) (ordinal_o v) x y)). rewrite ! ordinal_o_sr; split; move => [qa qb qc]; split => //; case: qc. - move => [sa sb sc]; constructor 1; split => //. split; [apply: (aux _ qa) | apply: (aux _ qb) | by case/ordo_leP: sc]. - move =>[sa sb sc]; constructor 2; split => //. split; [apply: (aux _ qa) | apply: (aux _ qb) | by case/ordo_leP: sc]. - by move => sa; constructor 3. - move => [sa sb /proj33 sc]; constructor 1; split => //. apply/ordo_leP; split => //. by case/ candu2P: qa => _; case => - [] // _; rewrite sa. by case/ candu2P: qb => _; case => - [] // _; rewrite sb. - move => [sa sb /proj33 sc]; constructor 2; split => //. apply/ordo_leP; split => //. by case/ candu2P: qa => _; case => - [] // _; rewrite sa. by case/ candu2P: qb => _; case => - [] // _; rewrite sb. - by move => sa; constructor 3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)