proposition: Theorem wf_slexprod : well_founded leA -> well_founded leB -> well_founded LexProd.
proof: Proof. intros; eapply wf_incl. - intros x y; apply slexprod_lexprod. - now apply wf_inverse_image, wf_lexprod. Qed.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image