This commit is contained in:
Thomas Baruchel 2023-01-23 23:00:55 +01:00
parent 24f147ebc0
commit 0bad6482ea
1 changed files with 4 additions and 1 deletions

View File

@ -1242,7 +1242,10 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
(* fin de la destructuration de a, désormais trop grand
cf. hypothèse I *)
simpl in I. apply eq_add_S in I. apply eq_add_S in I.
apply eq_add_S in I. apply eq_add_S in I.
symmetry in I. apply O_S in I. contradiction I.
Qed.