Работая с библиотекой Ensembles
, я хочу показать, что объединение Ensemble
с синглтоном не является Empty_set
.
Lemma aze: Singleton nat 1 <> Empty_set nat.
Однако я понятия не имею, как это доказать. Я был бы рад рассказать, что я пробовал, но, кроме игры с auto
, intro
и simpl
, я застрял.
H1 : Singleton nat 1 = Empty_set nat
(по intro H1
). Теперь вам нужно доказать False
.H2 : Empty_set nat -> False
.H2 : Singleton nat 1 -> False
через H1
.H3 : Singleton nat 1
.H2 H3 : False
.