proposition: Lemma In_result_rsize_leq r res : In r res -> rsize r < (list_size rsize res).
proof: Proof. funelim (list_size rsize res) => //=. case=> [-> | Hin]; [| have Hleq := (H r Hin)]; lia. Qed.
imports: List Coq(Lia ssreflect) Equations(Equations)