Merge pull request #16 from coq-community/mc_1110

Adapt to math-comp/math-comp#1110
coq-community · Nov 7, 2023 · 979da1e · 979da1e
2 parents 82583c0 + 8921194
commit 979da1e
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/theories/numbers/ssete7.v b/theories/numbers/ssete7.v
@@ -1309,7 +1309,7 @@ rewrite !muln1 mulnDl mulnC addnCA; congr (_ + _).
 Qed.
 
 
-Lemma F22 n: \sum_(i<n) i `! * i = n `! .-1.
+Lemma F22 n: \sum_(i<n) i `! * i = (n `! ).-1.
 Proof.
 elim: n; first by rewrite big_ord0.
 move => n Hrec;rewrite  big_ord_recr /=  Hrec {Hrec}.

diff --git a/theories/ordinals/sset15.v b/theories/ordinals/sset15.v
@@ -4731,7 +4731,7 @@ move: sc => [ix sx].
 have pf':~ (exists a : Set, cpow_less_ec_prop \2c x a).
   by move => [a [px py]]; case: pf; exists a.
 move: (cpow_less_ec_pr6 ix le22 pf') => eq1.
-have pa: (\2c ^c \cf (\2c ^<c x)) <c \2c ^<c x.
+have pa: (\2c ^c (\cf (\2c ^<c x))) <c \2c ^<c x.
   have pb:= (cofinality_small ix).
   move: (aux _ (conj pb sx)) => [b [p1 p2 p3]].
   by rewrite eq1; apply: (clt_leT p3); apply: cpow_less_pr2.

diff --git a/theories/sets/sset1.v b/theories/sets/sset1.v
@@ -111,7 +111,7 @@ Axiom IM_P :  forall (x : Set) (f : x -> Set) (y : Set),
 
 Axiom p_or_not_p: forall P:Prop,  P \/ ~ P.
 
-Lemma ixm (P: Prop): P + ~P.
+Lemma ixm (P: Prop): P + (~P).
 Proof.
 apply: (chooseT (fun _ => True)).
 by case: (p_or_not_p P) => H;constructor; [ left | right ].
@@ -1030,7 +1030,7 @@ Definition powerset (x : Set) :=
  IM (fun p : x -> C2 =>
     Zo x (fun y : Set => forall hyp : inc y x, Ro (p (Bo hyp)) = C0)).
 
-Notation "\Po E" :=   (powerset E) (at level 40).  
+Notation "\Po E" :=   (powerset E) (at level 30).
 
 Lemma setP_i y x : sub y x -> inc y (\Po x). 
 Proof.