|2: lapply (c ?? x H2) as H3; cases H3 (H4 H4); [right; assumption|cases (Lxy H4)]]
qed.
-theorem lt_to_excede: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
+theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
intros (E a b Lab); cases Lab (LEab Aab);
cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)
qed.