proposition: Lemma orsum_or: order (order_sum r g).
proof: Proof. move: osa=> [or sr alo]. rewrite /order_sum; set s := _ r g; set x:= _ g. have ->: (graph_on s x = graph_on (fun a b => [/\ inc a x, inc b x & s a b]) x). by apply : Zo_exten1 => t /setX_P [_ pa pb]; split => //;move => [_ _]. apply: order_from_rel; split => //; rewrite /s/order_sum_r. - move=> u v w [ux vx suv] [_ xw suw];split => //. case: suv; case: suw. + by left; order_tac. + by move=> [sq leq]; rewrite sq; left. + by move=> h [sq leq]; rewrite sq;left. + move=> [sq1 le1][sq2 le2]; right; split; first by ue. move: (du_index_pr1 ux) => [qdg _ _]. by rewrite - sq2 in le1; move: (alo _ qdg)=> ov; order_tac. - move=> u v [ux vx suv] [_ _ svu]. have [qudg puv pu] := (du_index_pr1 ux). have [qvdg pvv pv] := (du_index_pr1 vx). case: suv; case: svu. + move=> lt1 lt2; order_tac. + by move => [eq _] [_ lt1]; case: lt1. + by move => [_ lt1] [eq _]; case: lt1. + move=> [eq le1][_ le2]; rewrite eq in le1; move: (alo _ qudg) => ou. apply: pair_exten =>//;order_tac. - move=> u v [ux vx suv]. have [qudg puv pu] := (du_index_pr1 ux). have [qvdg pvv pv] := (du_index_pr1 vx). by split; split => //;right; split => //; [move: (alo _ qudg) | move: (alo _ qvdg) ] => ou; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)