proposition: Theorem make_partition_aux_correct : forall (n : nat) (f : nat -> nat), (forall i j : nat, In (i, j) (make_partition_aux f n) -> 1 <= i /\ i <= n /\ i < j /\ j = f i) /\ (forall i : nat, 1 <= i /\ i <= n /\ i < f i -> In (i, f i) (make_partition_aux f n)).
proof: Proof. intros n f; elim n; simpl in |- *; auto. split. intros i j H; elim H. intros i (H1, (H2, H3)); absurd (0 < i); auto with arith. intros n1 (Rec, Rec1); case (le_lt_dec (f (S n1)) (S n1)); simpl in |- *; auto. intros H; split. intros i j H1; case (Rec i j); auto. intros H2 (H3, H4); auto with arith. intros i (H1, (H2, H3)). case (le_lt_eq_dec _ _ H2); auto with arith. intros H4; absurd (f i <= i); auto with arith; rewrite H4; auto with arith. intros H; split. intros i j [H1| H1]; auto. injection H1. intros H2 H3; rewrite <- H2; rewrite <- H3; auto with arith. case (Rec i j); auto. intros H2 (H3, H4); auto with arith. intros i (H1, (H2, H3)). case (le_lt_eq_dec _ _ H2); auto with arith. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)