I made some record structure $I$ with addition and equality. And I made an axiom.
Axiom I_dec :
forall a : I, ({0 < a} + {a < 0}) + {a == 0}.
With this axiom, I define a multiplication of $I$.
Definition I_seq_mult_l (a b : I) :=
match (I_dec a) with
| inleft (left H) =>
match (I_dec b) with
| inleft (left H) => ...
| inleft (right H) => ...
| inright H => ...
end
| inleft (right H) =>
match (I_dec b) with
| inleft (left H) => ...
| inleft (right H) => ...
| inright H => ...
end
| inright H => ...
end.
When I prove some lemma, I meet an unsolved situation.
1 goal
a, b : I
Ha : const_I 0 < a
Hb : const_I 0 < b
Hb' : - b < const_I 0
______________________________________(1/1)
(exists m : positive,
forall n : positive,
(m <= n)%positive ->
-
match I_dec (- b) with
| inleft (left _) => ...
| inleft (right _) =>
fun n0 : positive => ...
| inright _ => ...
end n <= r a n * r b n)
Previously, I destruct (I_dec a) and (I_dec b).
destruct (I_dec a) as [[Ha|Ha]|Ha], (I_dec b) as [[Hb|Hb]|Hb].
I made a hypothesis Hb' from Hb. And I think Hb' implies that I_dec (- b) match with inleft (right _).
So I want to write 'simpl' and make this goal simple.
However, I can't do this. So, I destruct (I_dec (- b)) also. It multiplies steps three times.
Can I match a processed hypothesis with a part of a decidable axiom?