gistfile1.txt

In environment
Node : FinType.type
R : BoundedSemiring.type
Hcm : IsCommutativeMonoid.axioms_ R
Hsr : IsSemiring.axioms_ R Hcm
HmulC : ∀ a b : R, a * b = b * a
M : Matrix
H_total_order : ∀ x y : R, x + y = x ∨ x + y = y
a, b, c : Node
H_ab_le : mat_star M b a ≤ mat_star M a b
H_ab_ne : mat_star M b a ≠ mat_star M a b
H_bc_le : mat_star M c b ≤ mat_star M b c
H_bc_ne : mat_star M c b ≠ mat_star M b c
S := mat_star M : Matrix
H_ca_le_ac : S a c + S c a = S a c
Heq : S c a = S a c
Htmp1 : S a b * S b c ≤ S c a
Htmp2 : S b c * S c a ≤ S b a
Htmp3 : S a b * S b c * S b c ≤ S c a * S b c
The term
"match HmulC (S c a) (S b c) in (_ = y) return
(S c a * S b c
≤ y) with
| eq_refl => ?o
end" has type
"@Orel
(Structures_Semiring__to__Structures_CommutativeMonoid
(Structures_BoundedSemiring__to__Structures_Semiring
R))
(@mul
(Structures_BoundedSemiring__to__Structures_Semiring
R) (S c a) (S b c))
(@mul
{|
Semiring.sort := BoundedSemiring.sort R;
Semiring.class :=
{|
Semiring.Structures_IsCommutativeMonoid_mixin :=
Hcm;
Semiring.Structures_IsSemiring_mixin := Hsr
|}
|} (S b c) (S c a))"
while it is expected to have type
"@Orel
(Structures_Semiring__to__Structures_CommutativeMonoid
(Structures_BoundedSemiring__to__Structures_Semiring
R))
(@mul
(Structures_BoundedSemiring__to__Structures_Semiring
R) (S c a) (S b c))
(@mul
(Structures_BoundedSemiring__to__Structures_Semiring
R) (S b c) (S c a))".