In Coq, destruct more or less corresponds to a case analysis. It is similar to induction except that there's no induction hypothesis. Here is a (admittedly rather trivial) example of this tactic:
Require Import Coq.Arith.Lt.
Theorem atLeastZero : forall a,
0 <= a.
Proof.
intros.
destr...
