証明してみた。 - 菊やんの雑記帳http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。 とりあえず、問題設定 Axiom A : Set. Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }. Axiom A_mul : A -> A -> A. Axiom A_zero: A. Axiom A_one: A. Infix "*" := A_mul. Notation "0" := A_zero. Notation "1" := A_one. Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c). Axiom A_mul_comm: forall a b, a * b = b * a. Axiom A_mul_1_r: forall a,
