[ true ⇒ pred fx
| false ⇒ fx
]);
- elim (H f' ? ? x);
- [ simplify in H5;
- clear f';
- elim H5;
- clear H5;
- apply (ex_intro ? ? a);
- split;
- [ generalize in match H4;
- clear H4;
- rewrite < H6;
- clear H6;
- apply (ltb_elim (f (S n1)) (f a));
- [ (* TODO: caso impossibile (uso l'iniettivita') *)
- simplify;
- | simplify;
- intros;
- reflexivity
- ]
- | apply le_S;
+ cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+ [ elim (H f' ? ? x);
+ [ simplify in H5;
+ clear Hcut;
+ clear f';
+ elim H5;
+ clear H5;
+ apply (ex_intro ? ? a);
+ split;
+ [ generalize in match H4;
+ clear H4;
+ rewrite < H6;
+ clear H6;
+ apply (ltb_elim (f (S n1)) (f a));
+ [ (* TODO: caso impossibile (uso l'iniettivita') *)
+ simplify;
+ | simplify;
+ intros;
+ reflexivity
+ ]
+ | apply le_S;
+ assumption
+ ]
+ | apply Hcut
+ | simplify;
+ intro;
+ apply (ltb_elim (f (S n1)) (f m));
+ simplify;
+ intro;
+ [ generalize in match (H2 m);
+ intro;
+ change in match n1 with (pred (S n1));
+ apply le_to_le_pred;
+ assumption
+ | generalize in match (H2 (S n1));
+ intro;
+ generalize in match (not_lt_to_le ? ? H5);
+ intro;
+ generalize in match (transitive_le ? ? ? H7 H6);
+ intro;
+ (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *)
+ ]
+ | rewrite > (pred_Sn n1);
+ simplify;
+ generalize in match (H2 (S n1));
+ intro;
+ generalize in match (lt_to_le_to_lt ? ? ? H4 H5);
+ intro;
+ unfold lt in H6;
+ apply le_S_S_to_le;
assumption
]
- | (* This branch proves injectivity of f' *)
+ | intros 4;
+ unfold f';
simplify;
- intros 4;
apply (ltb_elim (f (S n1)) (f x1));
simplify;
apply (ltb_elim (f (S n1)) (f y));
apply le_S;
assumption
]
- | simplify;
- intro;
- apply (ltb_elim (f (S n1)) (f m));
- simplify;
- intro;
- [ generalize in match (H2 m);
- intro;
- change in match n1 with (pred (S n1));
- apply le_to_le_pred;
- assumption
- | generalize in match (H2 (S n1));
- intro;
- generalize in match (not_lt_to_le ? ? H5);
- intro;
- generalize in match (transitive_le ? ? ? H7 H6);
- intro;
- (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *)
- ]
- | rewrite > (pred_Sn n1);
- simplify;
- generalize in match (H2 (S n1));
- intro;
- generalize in match (lt_to_le_to_lt ? ? ? H4 H5);
- intro;
- unfold lt in H6;
- apply le_S_S_to_le;
- assumption
]
]
].