proposition: Lemma Exercise2_7A2 r r': order r -> order r' -> has_greatest r' -> inductive (order_sum2 r r').
proof: Proof. move=> or or' [u ug];apply: Exercise2_7B6. by move: (orsum2_greatest' or or' ug)=> h; exists (J u C1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)