Stream: math-comp analysis

Topic: propeqE error


view this post on Zulip vlj (Oct 04 2020 at 11:07):

Hi,
I have a lemma : Lemma subsetNeqSetDnonempty {T} (X Y : set T) (H : X `<=` Y) : X != Y <-> (Y `\` X) != set0. that I managed to prove. I'd like to convert it to an equality instead of an equivalence: Lemma subsetNeqSetDnonemptybis {T} (X Y : set T) (H : X `<=` Y) : (X != Y) = ((Y `\` X) != set0).. However when I try to do rewrite propeqE at the very beginning, I get an error The LHS of propeqE (_ = _) does not match any subterm of the goal. Is it because I have an hypothesis H ? I noticed that it works if I change the goal to ((X `<=`Y) /\ X!=Y) = ((Y `\` X) != set0) but I don't understand why.


Last updated: Mar 28 2024 at 22:01 UTC