Update
This commit is contained in:
parent
03aa9cd43f
commit
24f9104737
|
@ -425,6 +425,7 @@ Proof.
|
||||||
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
|
||||||
generalize Z. generalize H3. apply Nat.lt_trans.
|
generalize Z. generalize H3. apply Nat.lt_trans.
|
||||||
|
|
||||||
|
(* FIRST PART OF THE PROOF: case b0 = b1 *)
|
||||||
(* première hypothèse b0 = b1 mais alors on construit vers la
|
(* première hypothèse b0 = b1 mais alors on construit vers la
|
||||||
gauche jusqu'à (lest hd) et l'on a dans l'ordre jusqu'au centre :
|
gauche jusqu'à (lest hd) et l'on a dans l'ordre jusqu'au centre :
|
||||||
b1 | (negb b1) b1 | b1 (negb b1 ||
|
b1 | (negb b1) b1 | b1 (negb b1 ||
|
||||||
|
@ -580,7 +581,9 @@ Proof.
|
||||||
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
apply tm_step_cubefree in H. contradiction H. reflexivity.
|
||||||
apply Nat.lt_0_succ. reflexivity. easy. easy.
|
apply Nat.lt_0_succ. reflexivity. easy. easy.
|
||||||
|
|
||||||
|
(* SECOND PART PF THE PROOF: case b0 <> b1 *)
|
||||||
|
assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
|
||||||
|
rewrite e in H.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user