∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {s t u : V},
  G.degree s = G.degree u →
    (G.replaceVertex s t).degree s = G.degree s →
      (G.replaceVertex s t).degree u = G.degree u - 1 →
        0 < G.degree u →
          G.edgeFinset.card < G.edgeFinset.card + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u