Ssreflect Users Discussion List

[Cyril <>]

Hi!
We often have lemma of the form a = (b && c) and we want to rewrite right
to left knowing that b is true of knowing that c is true.

For example properEneq, expn_eq0, expf_eq0, poly_unitE, ...

I suggest to add the following lemma to ssrbool. What do you think? I'm not
fond of the naming I chose, do you have suggestions?

Lemma rew_condAl (a b c : bool) : a = (b && c) -> (c -> b = a).
Lemma rew_condAr (a b c : bool) : a = (b && c) -> (b -> c = a).

And for the sake of exhaustivity:

Lemma rew_condVr (a b c : bool) : a = (b || c) -> (~~ b -> c = a).
Lemma rew_condVl (a b c : bool) : a = (b || c) -> (~~ c -> b = a).

Lemma rew_condDr (a b c : bool) : a = (b (+) c) -> (~~ b -> c = a).
(*useless so far*)
Lemma rew_condDl (a b c : bool) : a = (b (+) c) -> (~~ c -> b = a).
(*useless so far*)

Best,
-- 
Cyril