- apply (nat_compare_elim (f (S n1)) x);
- [ (* TODO: caso complicato, ma simile al terzo *)
- | intros;
- apply (ex_intro ? ? (S n1));
- split;
- [ assumption
- | constructor 1
- ]
- | intro;
- letin f' ≝
- (λx.
- let fSn1 ≝ f (S n1) in
- let fx ≝ f x in
- match ltb fSn1 fx with
- [ true ⇒ pred fx
- | false ⇒ fx
- ]);
- cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
- [ cut (∀x. x ≤ n1 → f' x ≤ n1);
- [ elim (H f' ? ? x);
+ letin f' ≝
+ (λx.
+ let fSn1 ≝ f (S n1) in
+ let fx ≝ f x in
+ match ltb fSn1 fx with
+ [ true ⇒ pred fx
+ | false ⇒ fx
+ ]);
+ cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+ [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+ [ apply (nat_compare_elim (f (S n1)) x);
+ [ intro;
+ elim (H f' ? ? (pred x));
+ [ simplify in H5;
+ clear Hcut;
+ clear Hcut1;
+ clear f';
+ elim H5;
+ clear H5;
+ apply (ex_intro ? ? a);
+ split;
+ [ generalize in match (eq_f ? ? S ? ? H6);
+ clear H6;
+ intro;
+ rewrite < S_pred in H5;
+ [ generalize in match H4;
+ clear H4;
+ rewrite < H5;
+ clear H5;
+ apply (ltb_elim (f (S n1)) (f a));
+ [ simplify;
+ intros;
+ rewrite < S_pred;
+ [ reflexivity
+ | apply (ltn_to_ltO ? ? H4)
+ ]
+ | simplify;
+ intros;
+ generalize in match (not_lt_to_le ? ? H4);
+ clear H4;
+ intro;
+ generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
+ intro;
+ generalize in match (H1 ? ? ? ? H4);
+ [ intro;
+ |
+ |
+ ]
+ ]
+ | apply (ltn_to_ltO ? ? H4)
+ ]
+ | apply le_S;
+ assumption
+ ]
+ | apply Hcut
+ | apply Hcut1
+ | apply le_S_S_to_le;
+ rewrite < S_pred;
+ exact H3
+ ]
+ (* TODO: caso complicato, ma simile al terzo *)
+ | intros;
+ apply (ex_intro ? ? (S n1));
+ split;
+ [ assumption
+ | constructor 1
+ ]
+ | intro;
+ elim (H f' ? ? x);