Skip to content
Snippets Groups Projects
Commit 02c93102 authored by Mouhcine's avatar Mouhcine
Browse files

comment the prove of kronecker_bigop_scal_in_l to compile

parent 3e518c9b
No related branches found
No related tags found
No related merge requests found
......@@ -139,11 +139,11 @@ Proof.
intros n j a.
induction n.
(* *)
erewrite <- bigop_plus_0.
(*erewrite <- bigop_plus_0.
f_equal.
admit.
apply functional_extensionality; intros i; f_equal.
*)
(*
rewrite bigop_plus_0; easy.
(* *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment