The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

Using grobner basis it works:

Require Import Reals Nsatz.

Open Scope R_scope.

Section F.

Variables m11 m12 m13
          m21 m22 m23
          m31 m32 m33 : R.
Hypothesis Hd :
  m11 * m22 * m33 + m12 * m23 * m31 + m13 * m21 * m32 -
  m31 * m22 * m13 - m32 * m23 * m11 - m33 * m21 * m12 = 1.

Variable   H1 : m11 ^2 + m21 ^2 + m31^2  = 1%R.
Variable   H2 : m12 ^2 + m22 ^2 + m32^2  = 1%R.
Variable   H3 : m13 ^2 + m23 ^2 + m33^2  = 1%R.
Variable   H4 : m11 * m12 + m21 * m22 + m31 * m32 = 0%R.
Variable   H5 : m11 * m12 + m21 * m23 + m31 * m33 = 0%R.
Variable   H6 : m12 * m13 + m22 * m23 + m32 * m33 = 0%R.

Let x := m32 - m23.
Let y := m13 - m31.
Let z := m21 - m12.


Lemma F1 : (m11 * x + m12 * y + m13 * z)   = x.
Proof.
simpl in H1, H2, H3.
nsatz.
Qed.

Lemma F2 : (m21 * x + m22 * y + m23 * z)   = y.
Proof.
simpl in H1, H2, H3.
nsatz.
Qed.

Lemma F3 : (m31 * x + m32 * y + m33 * z)   = z.
Proof.
simpl in H1, H2, H3.
nsatz.
Qed.

--
Laurent