proposition: Fact rem_2_mult x y : rem (x*y) 2 = 1 <-> rem x 2 = 1 /\ rem y 2 = 1.
proof: Proof. generalize (rem_2_is_0_or_1 x) (rem_2_is_0_or_1 y). do 2 rewrite <- rem_mult_rem, Nat.mul_comm. intros [ H1 | H1 ] [ H2 | H2 ]; rewrite H1, H2; simpl; rewrite rem_lt; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)