Bot -> Invalid rename, fixpoint move

diaframe/lib/greatest_fixpoint.v

-From iris.bi Require Export bi telescopes lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.fixpoint_mono.
 From iris.proofmode Require Import proofmode environments classes_make.
 From diaframe Require Import proofmode_base.
 

diaframe/lib/own_hints.v

@@ -335,7 +335,7 @@ From stdpp Require Import telescopes.
 Section other.
 
   Global Instance excl_inhabited {A : ofe} : Inhabited (exclR A).
-  Proof. split. by apply ExclBot. Qed.
+  Proof. split. by apply ExclInvalid. Qed.
 
   Global Arguments option_unit_instance /.
 
@@ -998,14 +998,14 @@ Section validity.
       by iRewrite "Ha".
     Qed.
     Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-      IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+      IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
     Proof. 
       split; rewrite /op /= /cmra_op //=; eauto.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
       rewrite /validN /= /cmra_validN //=.
     Qed.
     Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-      IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+      IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
     Proof. 
       split; rewrite /op /= /cmra_op //=; eauto.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
@@ -1482,7 +1482,7 @@ Section validity.
     Qed.
 
     Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
-      IsValidOp ExclBot a1 a2 Σ False%I.
+      IsValidOp ExclInvalid a1 a2 Σ False%I.
     Proof. split; rewrite excl_validI /=; eauto. Qed. *)
     Lemma excl_subtract {O : ofe} (o1 o2 : O) : (* this one is bad for recursive instances *)
       TCIf (SolveSepSideCondition (¬ (o1 ≡ o2))) False TCTrue →