proposition: Lemma mkciph_eq (m m': Word) (r r': Key): (mkciph m r == mkciph m' r') = (m == m') && (r == r').
proof: Proof. case: (eq_dec ((m == m') && (r == r')) true). 1: { move=> /andP [/eqP -> /eqP ->]. by rewrite !eq_refl. } move /eqP. rewrite eqb_id => /nandP [/negPf Hneq|/negPf Hneq]. all: rewrite Hneq ?Bool.andb_false_r /=. all: move /eqP in Hneq. all: apply /eqP => contra. all: apply (f_equal ciph_to_pair) in contra. all: rewrite !ciph_to_pair_mkciph in contra. all: by case: contra. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)