proposition: Lemma orsum2_osr: order_on (order_sum2 r r') (canonical_du2 (substrate r) (substrate r')).
proof: Proof. move: cdo_wor => [[ord _ ] sr]. have aw: orsum_ax canonical_doubleton_order (variantLc r r'). by split => //; aw; fprops. split; first by apply: orsum_or. rewrite orsum_sr // /canonical_du2 /order_sum2 /sum_of_substrates. rewrite canonical2_substrate //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)