proposition: Lemma contractive_to_invariant : forall I A (M:family I A) (F:A->A) (Q:I->A->Prop), OFE M -> contractive M F Q -> invariant M F Q.
proof: Proof. Proof using. introv Ofem Cont. intros_all. forwards~ [M1 M2]: (>> Cont i x x). introv Rji. splits~. apply~ refl_inv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)