lapply (is_positive_denominator_Qinv (Qinv q));
[ rewrite > Qinv_Qinv in Hletin;
assumption
- | generalize in match H; elim q; assumption]
+ | elim q in H ⊢ %; assumption]
qed.
theorem is_negative_enumerator_Qinv:
lapply (is_negative_denominator_Qinv (Qinv q));
[ rewrite > Qinv_Qinv in Hletin;
assumption
- | generalize in match H; elim q; assumption]
+ | elim q in H ⊢ %; assumption]
qed.