feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>