proposition: Theorem make_partition_correct : forall n : nat, (forall i j k l : nat, In (i, j) (make_partition n) /\ In (k, l) (make_partition n) -> (i = k <-> j = l) /\ i <> l /\ j <> k) /\ (forall i : nat, 1 <= i /\ i <= 2 * n -> exists j : nat, In (i, j) (make_partition n) \/ In (j, i) (make_partition n)) /\ (forall i j : nat, In (i, j) (make_partition n) -> (1 <= i /\ i <= 2 * n) /\ 1 <= j /\ j <= 2 * n) /\ (forall i j : nat, In (i, j) (make_partition n) -> prime (i + j)).
proof: Proof. intros n; unfold make_partition in |- *. case (Partition n). intros f Hf; split. intros i j k l (H1, H2). case (make_partition_aux_correct (2 * n) f); intros HR1 HR2. case (HR1 _ _ H1); intros H3 (H4, (H5, H6)). case (HR1 _ _ H2); intros H7 (H8, (H9, H10)). case (Hf i); auto with arith; intros H11 (H12, ((H13, H14), H15)). case (Hf k); auto with arith; intros H16 (H17, ((H18, H19), H20)). split; split. intros H21; apply trans_equal with (1 := H6); apply trans_equal with (2 := sym_equal H10); apply f_equal with (f := f); auto with arith. intros H21; apply trans_equal with (1 := sym_equal H12); apply trans_equal with (2 := H17); apply f_equal with (f := f); auto with arith; apply trans_equal with (1 := sym_equal H6); apply trans_equal with (1 := H21); auto. red in |- *; intros H21; absurd (j <= i); auto with arith. rewrite H6; rewrite H21; rewrite H10; rewrite H17; rewrite <- H10; auto with arith. red in |- *; intros H21; absurd (l <= k); auto with arith. rewrite H10; rewrite <- H21; rewrite H6; rewrite H12; rewrite <- H6; auto with arith. split. intros i (H1, H2); exists (f i). case (make_partition_aux_correct (2 * n) f); intros HR1 HR2. case (Nat.le_gt_cases i (f i)); intros H3. case (le_lt_eq_dec _ _ H3); intros H4; auto with arith. left; apply HR2; repeat (split; auto with arith). case (Hf i); auto with arith. intros H5; case H5; auto. right; case (Hf i); auto with arith. intros H4 (H5, ((H6, H7), H8)). pattern i at 2 in |- *; rewrite <- H5. apply HR2; repeat (split; auto with arith). rewrite H5; auto. split. intros i j H1. case (make_partition_aux_correct (2 * n) f); intros HR1 HR2. case (HR1 _ _ H1). intros H2 (H3, (H4, H5)); split; auto. rewrite H5; case (Hf i); auto with arith. intros H6 (H7, ((H8, H9), H10)); auto. intros i j H1. case (make_partition_aux_correct (2 * n) f); intros HR1 HR2. case (HR1 _ _ H1). intros H2 (H3, (H4, H5)); auto. rewrite H5; auto. case (Hf i); auto with arith. rewrite (Nat.add_comm i); intuition. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)