proposition: Lemma repcode_MD_decoding r : MD_decoding [set cw in Rep.code r] (Decoder.repair (Lcode.dec (Rep.Lcode_wo_repair (@reprepair_img r)))).
proof: Proof. move=> /= u; rewrite /MD_decoding_alt => /= v uv w. rewrite Rep.codewords !inE => /orP wC. move: uv; rewrite /repair ffunE. move H : (majority_vote _ _) => [h | //]. case=> <-. move: H; rewrite /majority_vote; case: ifPn. move=> Hr [<-{h}]; case: wC => /eqP -> //. rewrite 2!dH_num_occ_opp {2}/negF2 eqxx; exact: num_occ_tuple_F2. rewrite -leqNgt => H. case: ifPn => //. rewrite negb_and negbK. case/orP => H1 [<-{h}]. - case: wC => /eqP -> //. rewrite 2!dH_num_occ_opp; apply num_occ_tuple_F2. rewrite (_ : N(_ | _) = r.+1 - N(1%R | tuple_of_row u))%nat; last first. rewrite -[in X in _ = (X - _)%nat](num_occ_negF2 1%R (tuple_of_row u)). by rewrite addnC addnK. rewrite (@leq_ltn_trans (r.+1 - (r.+1)./2)%nat) //. by rewrite -{2}(odd_double_half r.+1) -addnn addnA addnC addnA addnK leq_addr. apply ltn_sub2l; last by rewrite ltn_neqAle H eq_sym H1. rewrite (leq_ltn_trans H) //. rewrite -ltn_double (_ : _./2.*2 = r.+1 - odd r.+1)%nat; last first. by rewrite -{2}(odd_double_half r.+1) addnC addnK. by rewrite -addnn (@leq_ltn_trans r.+1) // ?leq_subr // addnS ltnS ltn_addr. - case : wC => /eqP -> //. rewrite 2!dH_num_occ_opp; apply num_occ_tuple_F2. rewrite (_ : N(_ | _) = r.+1 - N(1%R | tuple_of_row u))%nat; last first. rewrite -[in X in _ = (X - _)%nat](num_occ_negF2 1%R (tuple_of_row u)). by rewrite addnC addnK. rewrite -ltn_double (_ : _./2.*2 = r.+1 - odd r.+1)%nat; last first. by rewrite -{2}(odd_double_half r.+1) addnC addnK. rewrite H1 /= subn1 /= doubleB. rewrite (@leq_trans ((r.+1).*2 - (r.+1)./2.*2)%nat) //; last first. by rewrite leq_sub2l // leq_double. rewrite (_ : (r.+1)./2.*2 = r.+1 - odd r.+1)%nat; last first. by rewrite -{2}(odd_double_half r.+1) addnC addnK. rewrite subnBA //; last by case: (odd r.+1). by rewrite -addnn -addnA addnC addnK ltn_addr. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code