New lemmas for stdlib

[namasikanam]

This is the first part of the auxiliary lemmas used in the oram proofs. My current plan is to create 5 PRs (~2k LoC) in total.

I will make sure all the proofs are either written by human, or first generated by LLM and then carefully edited step by step by myself.

[oskgo]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

[namasikanam]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

Thanks. This makes lots of sense. I feel that I learned the proper way of handling option. I removed the all lemmas related to option except the following one, which I feel useful and I hope it's also useful for others.

lemma oget_ext ['a] (x y : 'a option) :
     x <> None
  => y <> None
  => oget x = oget y
  => x = y.
proof. by case x; case y. qed.