proposition: Lemma wf_lexico : well_founded lexico.
proof: Proof. pose (R := fun p q : A * B => lexprod A (fun _ : A => B) ltA (fun _ : A => ltB) (pair2sig p) (pair2sig q)). apply wf_incl with R. - intros p q H; destruct p, q; red. destruct H. + now left. + now right. - unfold R;apply wf_inverse_image, wf_lexprod. + trivial. + intro; trivial. Defined.
imports: Coq(Relations Wellfounded.Lexicographic_Product Wellfounded.Inverse_Image Wellfounded.Inclusion Setoid)