前回の続き。
assert((n>1->n=n+0)->(S n>1->n=n+0)).
より
assert((n>1->n=n+0)->(S n>1->S n=S n+0)).
のほうがエレガントですかね。
例1
Lemma l3_2: forall (n:nat), n>1 -> n=n+0. Proof. intros. induction n. reflexivity. (* ここがポイント *) assert((n>1->n=n+0)->(S n>1->S n=S n+0)). omega. apply H0 in IHn. apply IHn. apply H. Qed.
例2
Lemma l4_3: forall (a b:nat), 1<a -> 1<b -> 1<a*b. Proof. intros. induction a. assert(1<0->False). omega. apply H1 in H. apply False_ind. auto. (* ここがポイント *) assert((1<a -> 1<a*b)->(1<S a -> 1<S a*b)). intros. apply gt_S in H2. destruct H2 as [ HA | HB ]. simpl. omega. rewrite <- HB. omega. apply H1 in IHa. apply IHa. apply H. Qed.
例3（！）
Theorem Erdos_Straus_conjecture: forall (n x y z x' y' z':nat), n>1 -> x>1 -> y>1 -> z>1 -> (2 = 1/x +1/y +1/z) /\ (x'<>2/\x'<>3) /\ (y'<>2/\y'<>3) /\ (z'<>2/\z'<>3) /\ (4 <> n*(1/x +1/y +1/z)) -> 4 <> 3*(1/x' +1/y' +1/z'). Proof. intros. destruct H3 as [ H3 H4 ]. destruct H4 as [ H4 H5 ]. destruct H5 as [ H5 H6 ]. destruct H6 as [ H6 H7 ]. induction n. assert(0>1->False). omega. apply H8 in H. apply False_ind. auto. assert((n>1 -> (4 <> n*(1/x+1/y+1/z)) -> (4<>3*(1/x'+1/y'+1/z'))) -> (S n>1 -> (4 <>S n*(1/x+1/y+1/z)) -> (4<>3*(1/x'+1/y'+1/z')))). intros. apply gt_S in H9. destruct H9 as [ HA | HB ]. omega. rewrite <- HB in H7. rewrite <- H3 in H7. assert(4<>2*2->False). omega. apply H9 in H7. apply False_ind. auto. apply H8 in IHn. apply IHn. apply H. apply H7. Qed.
