proposition: Lemma reverse_lookup_Some l i x : reverse l !! i = Some x ↔ l !! (length l - S i) = Some x ∧ i < length l.
proof: Proof. split. - destruct (decide (i < length l)); [ by rewrite reverse_lookup|]. rewrite lookup_ge_None_2; [done|]. rewrite reverse_length. lia. - intros [??]. by rewrite reverse_lookup. Qed.
imports: stdpp(options)