I want to prove Lemma leq_exp2lp n1 n2 : 0 < n1 -> n1 <= n2 -> x ^ n1 and Theorem Argand : (x^2 + x + 1) * (x^2 - x + 1) = x^4 + x^2 + 1. in Coq

Question

As I say in title, I want to prove two Lemmata in math-comp.

At first,

======code======

From mathcomp Require Import all_ssreflect.

Section Argand.

Variable x : nat.

Lemma leq_exp2lp n1 n2 : 0 < n1 -> n1 <= n2 -> x ^ n1 <= x ^ n2.

Proof. move=> H1 H2.

Search (_ ^ _ <= _ ^ ).

case (posnP x). move=> xO.

Search "^".

rewrite xO.

rewrite exp0n.

rewrite exp0n.

done.

Search (_ < _).

==================

From this, I don't know what should I do to prove.

Next,

====The content of lemma======

Lemma Argand : (x^2 + x + 1) * (x^2 - x + 1) = x^4 + x^2 + 1.

==============================

I think subn_sqr is useful to solve, but I can't transform the above equation into the forms applicable to subn_sqr.

Please, help me.

Answer 1

Without using MathComp, instead using standard library.

Require Import Arith Lia.

Section Argand.

  Variable x : nat.

  Lemma leq_exp2lp n1 n2 : 0 < n1 -> n1 <= n2 -> x ^ n1 <= x ^ n2.
  Proof.
    intros. destruct x.
    + repeat rewrite Nat.pow_0_l; try lia.
    + apply Nat.pow_le_mono_r; try lia.
  Qed.

  Theorem Argand : (x^2 + x + 1) * (x^2 - x + 1) = x^4 + x^2 + 1.
  Proof.
    simpl. nia.
  Qed.

End Argand.

And a bit later with your imports.

From mathcomp Require Import all_ssreflect.

Section Argand.

  Variable x : nat.

  Lemma leq_exp2lp n1 n2 : 0 < n1 -> n1 <= n2 -> x ^ n1 <= x ^ n2.
  Proof.
    intros. destruct x.
    + Search (0 ^ _ = 0). repeat rewrite exp0n.
      - auto.
      - Search (_ <= _ -> _ <= _ -> _ <= _). apply (leq_trans H H0).
      - auto.
    + Search (_ ^ _ <= _ ^ _). apply leq_pexp2l.
      - auto.
      - auto.
  Qed.

  (* ???? *)
  Lemma n_minus_n_is_zero n : n - n = 0.
  Proof.
    replace n with (0 + n) by ring. Search (_ + _ - _). rewrite subnDr. auto.
  Qed.

  Lemma Argand : (x^2 + x + 1) * (x^2 - x + 1) = x^4 + x^2 + 1.
  Proof.
    assert (x ^ 2 + x + 1 = x ^ 2 + 1 + x) by ring.
    assert (x ^ 2 - x + 1 = x ^ 2 + 1 - x).
    { clear H. unfold expn. simpl.
      Search (_ - _ + _ = _ + _ - _).
      apply addnBAC.
      pose proof (leq_exp2lp 1 2 ltac:(auto) ltac:(auto)).
      auto. }
    rewrite H H0. clear H H0.
    replace ((x ^ 2 + 1 + x) * (x ^ 2 + 1 - x)) with ((x ^ 2 + 1 - x) * (x ^ 2 + 1 + x)) by ring.
    rewrite <- subn_sqr. ring_simplify ((x ^ 2 + 1) ^ 2). simpl.
    Search (_ + _ - _). rewrite <- addnBAC.
    + f_equal. Search (_ + _ - _). rewrite <- addnBA.
      - f_equal. replace (2 * x ^ 2) with (x ^ 2 + x ^ 2) by ring.
        rewrite <- addnBA.
        * rewrite n_minus_n_is_zero. ring.
        * auto.
      - replace (2 * x ^ 2) with (x ^ 2 + x ^ 2) by ring.
        Search (_ <= _ + _). apply leq_addr. 
    + replace (x ^ 4 + 2 * x ^ 2) with (x ^ 2 + (x ^ 4 + x ^ 2)) by ring.
      apply leq_addr.
  Qed.

End Argand.

Probably MathComp users can make the second part much shorter. Making this into community wiki.