proposition: Theorem godel_coding_2357 : godel_coding 4.
proof: Proof. exists pos4_2357 (fun v => ⦉v#>pos0,v#>pos1,v#>pos2,v#>pos3⦊). + apply pos4_2357_gt_0. + intros p; repeat invert pos p; intros v ->. * rewrite combi_2357_2_0; apply not_divides_2_357. * rewrite combi_2357_3_0; apply not_divides_3_257. * rewrite combi_2357_5_0; apply not_divides_5_237. * rewrite combi_2357_7_0; apply not_divides_7_235. + intros p; repeat invert pos p; intros v; rew vec. * apply combi_2357_mult2. * apply combi_2357_mult3. * apply combi_2357_mult5. * apply combi_2357_mult7. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils gcd prime pos vec)