From cc6ee10296a9c1607b6f3a30ee46ef0365f4adc2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 28 Jun 2024 13:49:35 +0200 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1223 --- theories/schutte/ssete9.v | 4 ++-- theories/stern/fibm.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v index ea24e4c..836788b 100644 --- a/theories/schutte/ssete9.v +++ b/theories/schutte/ssete9.v @@ -1918,7 +1918,7 @@ Lemma mul_int n m : \F n * \F m = \F (n *m)%N. Proof. case: n; first by rewrite T1mul0n. move => n;case: m; first by rewrite T1muln0 muln0. -by move => m /=; rewrite - mulnE mulnSr addnC. +by move=> m /=; rewrite -?mulnE mulnSr addnC. (* FIXME: remove -?mulnE when requiring Coq >= 8.21 *) Qed. Lemma mul_phi0 a b: phi0 (a + b) = phi0 a * phi0 b. @@ -3780,7 +3780,7 @@ Lemma T2addn0: right_id zero T2add. Proof. by case. Qed. Lemma add_int n m : \F n + \F m = \F (n +m)%N. Proof. -by case: n m => // n [ | m]; rewrite /= - ? addnS // - addnE addn0. +by case: n m => // n [ | m]; rewrite /= - ? addnS // -?addnE addn0. (* FIXME: remove -?addnE when requiring Coq >= 8.21 *) Qed. Lemma add_fin_omega n: \F n + omega = omega. diff --git a/theories/stern/fibm.v b/theories/stern/fibm.v index 56d9c95..e1aa931 100644 --- a/theories/stern/fibm.v +++ b/theories/stern/fibm.v @@ -3965,7 +3965,7 @@ apply:ZeckM_prop3; apply/andP; split. by elim:n (0) => // k H n /=; rewrite H eqxx. rewrite /Zeck_val - fib_sum !big_ord_recl /=. elim:n => [|n Hr];first by rewrite big_nil big_ord0. -by rewrite big_ord_recr - (eqP Hr) iota_Sr rev_rcons big_cons addnC. +by rewrite big_ord_recr 1?addnA -(eqP Hr) iota_Sr rev_rcons big_cons addnC. (* FIXME: change 1?addnA into addnA when requiring Coq >= 8.21 *) Qed.