proposition: Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)} (x1 x2 x3 : A) (y1 y2 y3 : B) : lexico (x1,y1) (x2,y2) → lexico (x2,y2) (x3,y3) → (lexico y1 y2 → lexico y2 y3 → lexico y1 y3) → lexico (x1,y1) (x3,y3).
proof: Proof. intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico. intros [|[??]] [?|[??]]; simplify_eq/=; auto. by left; trans x2. Qed.
imports: stdpp(numbers) stdpp(options)