proposition: Lemma Kop_proof x1 x2 x3 y1 y2 y3 : (x3 <= x2) && ((x3 == x2) ==> x1) -> (y3 <= y2) && ((y3 == y2) ==> y1) -> (x3 + y3 <= x2 + y2) && ((x3 + y3 == x2 + y2)%nat ==> x1 && y1).
proof: Proof. move=> /andP [Hx Hx1] /andP [Hy Hy1]. rewrite (@leq_trans (x3+y2)) ?leq_add2r //=. apply/implyP=> H3. move/implyP: Hx1 => ->. move/implyP: Hy1 => -> //. rewrite -(leq_add2r y3) (eqP H3) leq_add2l in Hx. by rewrite eqn_leq Hy Hx. rewrite -(leq_add2l x3) (eqP H3) leq_add2r in Hy. by rewrite eqn_leq Hx Hy. by rewrite leq_add2l Hy. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode