One can read the Coq documentation about
discriminate tactic here.
Were is this tactic actually defined?
Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.Sign up to join this community