proposition: Lemma lookup_replicate_None n x i : n ≤ i ↔ replicate n x !! i = None.
proof: Proof. rewrite eq_None_not_Some, Nat.le_ngt. split. - intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto. - intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2. Qed.
imports: stdpp(options)