proposition: Lemma decryption_undoes_encryption : msg = msg'.
proof: Proof. rewrite /msg'. destruct msg_hat as [msg_hat' Hmsg_hat] => /=. have : decode cyp_hat = Some (msg *m S). have -> : cyp_hat = (msg *m S) *m 'G + (z *m P^-1). rewrite /cyp_hat /cyp /pubkey mulmxDl -!mulmxA mulmxV ?mulmx1 //. by apply: unitmx_perm. rewrite ffunE /=. have H : msg *m S *m 'G \in kernel 'H. move/subsetP: (Encoder.enc_img (Lcode.enc C)); apply. apply/imsetP; exists (msg *m S) => //. by rewrite ffunE. move: bdd => /=; rewrite /bdd /= => -> //; last first. by rewrite /P -perm_mxV wH_perm_mx Hz. move: (@encode_discard (msg *m S *m 'G) H). rewrite ffunE => K. congr Some. apply: (@Syslcode.encode_inj _ _ _ Hdimlen CSM). by rewrite ffunE /= /Syslcode.encode ffunE. rewrite Hmsg_hat => -[] ->. rewrite -mulmxA mulmxV ?mulmx1 //; exact S_inv. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssralg_ext hamming linearcode decoding channel_code