proposition: Lemma sameSome_None_l : ∀ {A B : eqType} (x : option A) (y : option B), sameSome x y → x == None → y == None.
proof: Proof. intros A B x y hs hN. move: hN => /eqP hN. subst. apply /eqP. unfold sameSome in hs. destruct y. 1: discriminate. reflexivity. Qed.
imports: mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(Axioms Prelude pkg_core_definition pkg_composition pkg_notation RulesStateProb pkg_advantage pkg_lookup pkg_semantics pkg_heap pkg_invariants pkg_distr pkg_rhl pkg_tactics choice_type) Coq(Utf8 FunctionalExtensionality Setoids.Setoid Classes.Morphisms) Equations(Equations)