diff --git a/theories/numbers/ssetq1.v b/theories/numbers/ssetq1.v
index 32e5cbd..00023b2 100644
--- a/theories/numbers/ssetq1.v
+++ b/theories/numbers/ssetq1.v
@@ -2190,7 +2190,7 @@ Qed.
 End  BQdiffProps4.
 
 Lemma BQdiv_div_simp a b c: ratp a -> ratp b -> ratp c -> b <> \0q ->
-    (a /q b) /q (c /q b) = a /qc.
+    (a /q b) /q (c /q b) = a /q c.
 Proof.
 move => aq bq cq bnz. 
 move:  (QS_inv bq)  (QS_inv cq) => biq ciq.
diff --git a/theories/ordinals/sset12.v b/theories/ordinals/sset12.v
index ca3158a..21d6e0e 100644
--- a/theories/ordinals/sset12.v
+++ b/theories/ordinals/sset12.v
@@ -635,7 +635,7 @@ move => oa ob; split.
   - by right.
   - move => h; case:(limit_nonsucc' (osum_limit oa ov) h).
 case; first by move => [-> osa]; rewrite (osum0r oa).
-move => [c oc ->]; rewrite - (osum2_succ oa oc); exists (a+oc); fprops.
+move => [c oc ->]; rewrite - (osum2_succ oa oc); exists (a +o c); fprops.
 Qed.
 
   
@@ -4622,7 +4622,7 @@ Qed.
 Lemma all_der_p13 : f \0o <> \0o -> normal_ofs (g \0o).
 Proof.
 move => fz.
-have pa: forall i j, i <oj -> g \0o i <o g \0o j.
+have pa: forall i j, i <o j -> g \0o i <o g \0o j.
   move => i j ij;move:(ij)=> [[oi oj _] _].
   apply/(all_der_p10 OS0 OS0 oi oj); split => //.
   + move => _; apply: ord_ne0_pos; first by apply:(OS_all_der OS0 oj).
diff --git a/theories/ordinals/sset13b.v b/theories/ordinals/sset13b.v
index 4f3051c..7bb0c96 100644
--- a/theories/ordinals/sset13b.v
+++ b/theories/ordinals/sset13b.v
@@ -1256,7 +1256,7 @@ Qed.
 
 Definition oprod2_comm_P4 x y :=
   exists z gamma c1 c2,
-  [/\ cnfp_nz z, \0o <ooexp z \0c, ordinalp gamma & 
+  [/\ cnfp_nz z, \0o <o oexp z \0c, ordinalp gamma &
   [/\ natp c1, natp c2,
   x = cnf_val z,
   cnf_degree z = gamma *o c1 &
diff --git a/theories/ordinals/sset13c.v b/theories/ordinals/sset13c.v
index a8c8ca0..367a066 100644
--- a/theories/ordinals/sset13c.v
+++ b/theories/ordinals/sset13c.v
@@ -83,7 +83,7 @@ Lemma Vr_oor x e: ~inc e (cnf_exponents x) -> Vr x e = \0c.
 Proof. by move => h; rewrite /Vr (Vg_out_of_range h). Qed.
   
 Lemma cnf_nat_sum_p2 x y : cnfp x -> cnfp y ->  forall e,
-   Vr (x +#fy) e =  (Vr x e) +c  Vr y e.
+   Vr (x +#f y) e =  (Vr x e) +c  Vr y e.
 Proof.
 move => ox oy e.
 move:(cnf_sort_correct (cnf_nat_sum_range ox oy)).
@@ -107,7 +107,7 @@ Qed.
 
 
 Lemma cnf_nat_sum_p3 x y z : cnfp x -> cnfp y -> cnfp z ->
-  (forall e, Vr z e =  (Vr x e) +c  Vr y e) -> z = x +#fy.
+  (forall e, Vr z e =  (Vr x e) +c  Vr y e) -> z = x +#f y.
 Proof.
 move => ox oy oz hz.
 move:(cnfp_nat_sum ox oy) (cnf_nat_sum_p2 ox oy); set t := cnf_nat_sum x y.
diff --git a/theories/ordinals/sset16b.v b/theories/ordinals/sset16b.v
index 897e1d9..aeed119 100644
--- a/theories/ordinals/sset16b.v
+++ b/theories/ordinals/sset16b.v
@@ -275,7 +275,7 @@ Qed.
 Lemma nds_k_of_prop f:
    f \0c = \1c -> f \1c = \1c -> 
    (forall n, natp n -> \1c <c n ->
-              f n = ndsC (nds_k_of n) *c f (n -cnds_k_of n)) ->
+              f n = ndsC (nds_k_of n) *c f (n -c nds_k_of n)) ->
    forall n, natp n ->  f n = nds_sol n.
 Proof.
 move => f0 f1 hb.
diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v
index ed568b3..857aeab 100644
--- a/theories/schutte/ssete9.v
+++ b/theories/schutte/ssete9.v
@@ -2204,7 +2204,7 @@ Qed.
 
 Lemma nf_revCE u v: T1bad <> T1omega * u  + \F v.
 Proof.
-case: (altP (u=Pzero)); first by move => ->; case v.
+case: (altP (u =P zero)); first by move => ->; case v.
 move/mul_omega_limit;set w:=  (T1omega * u).
 case: v; first by rewrite T1addn0 => sa sb; move: sa; rewrite - sb.
 by move => v; case w => // a n b; case a.
diff --git a/theories/sets/sset7.v b/theories/sets/sset7.v
index 28b21fa..cb9ad16 100644
--- a/theories/sets/sset7.v
+++ b/theories/sets/sset7.v
@@ -712,7 +712,7 @@ Proof.
 split.
   move=> [or or' [otr otr' [f [t [sx iso]]]]];split => //.
   move: (isomorphism_worder_sub (ordinal_o_wor or') sx) =>[].
-  set g := iso_seg_fun _ _ => sw isg; exists (g \cof ), (target g); split => //.
+  set g := iso_seg_fun _ _ => sw isg; exists (g \co f), (target g); split => //.
   exact: (compose_order_is iso isg).
 move=> [or or' [f [t [[sx sxp] oi]]]]; split => //; split; fprops.
 by exists f, t. 
diff --git a/theories/sets/sset9.v b/theories/sets/sset9.v
index 54c3eb1..cc5eaf6 100644
--- a/theories/sets/sset9.v
+++ b/theories/sets/sset9.v
@@ -2685,7 +2685,7 @@ move=> [q1N r1N [aeq r1p]].
 rewrite aeq csumA - cprodDr.
 set q2:= (a +c q).
 have q2N: natp q2 by apply: NS_sum.
-have dp: (cdivision_prop ((B *c q2) +cr) B q2 r) by split. 
+have dp: (cdivision_prop ((B *c q2) +c r) B q2 r) by split.
 by move: (cquorem_pr (NS_sum (NS_prod BN q2N) r1N) BN q2N r1N dp) => [_].
 Qed.
 
@@ -4124,7 +4124,7 @@ Proof.
 move=> h.
 move:(cleR (CS_sum2 a b)).  
 move:(NS_sum (proj31 h)(proj32 h)).
-move: {1 3}(a+cb) => n nN; move: n nN a b h; apply:Nat_induction.
+move: {1 3}(a +c b) => n nN; move: n nN a b h; apply:Nat_induction.
   move => a b [aN bN cab] /cle0 /csum_nz [az bz].
   set H := cdivides_zero NS0.
   by rewrite az bz in cab;move: (card1_nz(esym (cab \0c H H))).
@@ -7980,7 +7980,7 @@ suff eq: (sn +c sn = aux).
   by rewrite csum_nn -nsp [RHS] even_half.
 rewrite /aux cprodC /sn nsp.
 rewrite nsp in nN.
-have fim: (forall i,  i <c (csucc p) -> (fun i=> i +c (p -ci)) i = p).
+have fim: (forall i,  i <c (csucc p) -> (fun i=> i +c (p -c i)) i = p).
   by move=> i /(cltSleP pN) => ilp; apply: cdiff_pr. 
 rewrite - (fct_sum_const1 nN fim).
 rewrite - (sum_of_sums (fun i => i) (fun i=> (p -c i)) (csucc p)).