proposition: Lemma wf_lt_pair : well_founded lt_pair.
proof: Proof. unfold lt_pair. apply wf_inverse_image. apply wf_lexprod. now apply Wf_nat.lt_wf. intros _; now apply wf_lt_type. Qed.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)