First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A function $f:2^U\to2^U$ (from subsets of $U$ to subsets of $U$) is monotone, if $A\subseteq B$ always implies $f(A)\subseteq f(B)$. A fixed point of $f$ is a set $A$ such that $f(A)=A$.
For monotone $f$ there always is a least fixed point $\mu f$, namely the intersection of all $A\subseteq U$ such that $f(A)\subseteq A$. Least means that for arbitrary fixed points $F$ we always have $\mu f\subseteq F$.
For an example, let $f_{\tt nat}$ be defined by $f_{\tt nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$. The function $f_{\tt nat}$ is the one-step closure function under the constructors $0$ and $+1$. The condition $f_{\tt nat}(A)\subseteq A$ means that $A$ is closed under the constructors $0$ and $+1$. The intersection means that the $\mu f_{\tt nat}$ contains only those elements which are in every set closed under the constructors. These happen to be the natural numbers.
The example shows how the inductive definition of natural numbers is the least fixed point of closure under the natural numbers' constructors. Generally, inductively defined sets are least fixed points of closure under constructors.
Dually, for monotone $f$ there also is a greatest fixed point $\nu f$, namely the union of all $A\subseteq U$, such that $f(A)\supseteq A$. Greatest means that for arbitrary fixed points $F$ we always have $\nu f\supseteq F$. To make the duality complete, let us note that intersection is the $\subseteq$-infimum and union the $\subseteq$-supremum and thus the $\supseteq$-infimum. So, in fact, greatest fixed points for $\subseteq$ are just least fixed points for $\supseteq$ and vice versa.
(Also, observe that the requirement of monotonicity is the same for $\subseteq$ as for $\supseteq$.)
Now, for proof techniques. Let us begin with the example of induction on natural numbers. To show that some property $P$ holds for all natural numbers, we show that $P(0)$ and that $P(n)$ implies $P(n+1)$. Viewing $P$ as a subset of $U$ (the set of all elements where the property holds), the proof obligation for natural induction is that $P$ is closed under $f_{\tt nat}$. Correctness of the proof technique of natural induction then follows from the definition of least fixed point: If $f_{\tt nat}(P)\subseteq P$, then $P$ is part of the intersection that forms $\mu f_{\tt nat}$, so the property holds throughout $\mu f_{\tt nat}$, that is $\mu f_{\tt nat}\subseteq P$.
Induction is just the generalization of the previous paragraph to arbitrary monotone $f$ instead of $f_{\tt nat}$. Coinduction is the dual of induction: The proof obligation is $f(P)\supseteq P$. This means that if $P$ holds on some element $x$, then $x$ is constructed using only base elements on which $P$ also holds.
So, instead of showing that the property survives application of constructors, we have to show that it survives deconstruction. Once the proof obiligation is satisfied, we obtain $\nu f\supseteq P$.
What good is the conclusion $\nu f\supseteq P$? Let us reconsider $P$ not as a property but as a subset of $U$. The conclusion of coinduction establishes that all elements of $P$ are well-formed members of the coinductivly defined set $\nu f$.
This is what happens in the example in What is coinduction? showing forall n, Infinite (from n)
. Here, $f$ is closure under the constructors of Infinite
(not of colist
!) and $P$ is the set of all terms of the form from n
for some n
.