proposition: Lemma oprod0l x: \0o *o x = \0o.
proof: Proof. rewrite /oprod2 /order_prod2 oprod_zero ?ordinal0_pr //. aw; exists C1 => //; aww. rewrite ordinal_o_set0;exact: (proj2(set0_wor)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)