proposition: Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)} (x : A) (y : B) : complement lexico y y → complement lexico (x,y) (x,y).
proof: Proof. intros ? [?|[??]]; [|done]. by apply (irreflexivity lexico x). Qed.
imports: stdpp(numbers) stdpp(options)