style ssreflect

[vblot]

Dans le style ssreflect on n'utilise pas destruct, mais case.
D'autre part on n'utilise pas non plus fold ou unfold, mais plutôt rewrite -/cste et rewrite /cste
Par exemple :

internship2019/src/arith.v

Lines 105 to 112 in 17e55db

	Lemma lognn : forall n, logn n n = prime n.
	Proof.
	move=> n.
	destruct (prime n)eqn:n_prime ; unfold logn ; rewrite n_prime //.
	destruct n as [|n] ; first inversion n_prime.
	rewrite /= edivn_def /= divnn modnn /=.
	by destruct n as [|n] ; first inversion n_prime.
	Qed.

s'écrit plutôt :

Lemma lognn : forall n, logn n n = prime n.
Proof.
  move=> n.
  case n_prime: (prime n) ; rewrite /logn n_prime //.
  case: n n_prime=> [|n] n_prime ; first inversion n_prime.
  rewrite /= edivn_def /= divnn modnn /=.
  by case: n n_prime=> [|n] n_prime ; first inversion n_prime.
Qed.