Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.