Commit 2020-10-08 13:27 48a36046

feat(logic/nontrivial): a tactic to summon nontrivial instances (#4374)

Given a goal `a = b` or `a ≤ b` in a type `α`, generates an additional hypothesis `nontrivial α`
(as otherwise `α` is a subsingleton and the goal is trivial).
Alternatively, given a hypothesis `a ≠ b` or `a < b` in a type `α`, tries to generate a `nontrivial α`
hypothesis from existing hypotheses using `nontrivial_of_ne` and `nontrivial_of_lt`.