Theorem weqfromprodofstn ( n m : nat ) : ⟦n⟧ × ⟦m⟧ ≃ ⟦n*m⟧. Proof. intros. induction ( natgthorleh m 0 ) as [ is | i ]. - assert ( i1 : ∏ i j : nat, i < n -> j < m -> j + i * m < n * m). + intros i j li lj. apply (natlthlehtrans ( j + i * m ) ( ( S i ) * m ) ( n * m )). * change (S i * m) with (i*m + m). rewrite natpluscomm. exact (natgthandplusl m j ( i * m ) lj ). * exact ( natlehandmultr ( S i ) n m ( natgthtogehsn _ _ li ) ). + set ( f := λ ij : ⟦n⟧ × ⟦m⟧, match ij with tpair _ i j => make_stn ( n * m ) ( j + i * m ) ( i1 i j ( pr2 i ) ( pr2 j ) ) end ). split with f. assert ( isinf : isincl f ). * apply isinclbetweensets. apply ( isofhleveldirprod 2 _ _ ( isasetstn n ) ( isasetstn m ) ). apply ( isasetstn ( n * m ) ). intros ij ij' e. destruct ij as [ i j ]. destruct ij' as [ i' j' ]. destruct i as [ i li ]. destruct i' as [ i' li' ]. destruct j as [ j lj ]. destruct j' as [ j' lj' ]. simpl in e. assert ( e' := maponpaths ( stntonat ( n * m ) ) e ). simpl in e'. assert ( eei : i = i' ). { apply ( pr1 ( natdivremunique m i j i' j' lj lj' ( maponpaths ( stntonat _ ) e ) ) ). } set ( eeis := invmaponpathsincl _ ( isinclstntonat _ ) ( make_stn _ i li ) ( make_stn _ i' li' ) eei ). assert ( eej : j = j' ). { apply ( pr2 ( natdivremunique m i j i' j' lj lj' ( maponpaths ( stntonat _ ) e ) ) ). } set ( eejs := invmaponpathsincl _ ( isinclstntonat _ ) ( make_stn _ j lj ) ( make_stn _ j' lj' ) eej ). apply ( pathsdirprod eeis eejs ). * intro xnm. apply iscontraprop1. apply ( isinf xnm ). set ( e := pathsinv0 ( natdivremrule xnm m ( natgthtoneq _ _ is ) ) ). set ( i := natdiv xnm m ). set ( j := natrem xnm m ). destruct xnm as [ xnm lxnm ]. set ( li := natlthandmultrinv _ _ _ ( natlehlthtrans _ _ _ ( natlehmultnatdiv xnm m ( natgthtoneq _ _ is ) ) lxnm ) ). set ( lj := lthnatrem xnm m ( natgthtoneq _ _ is ) ). split with ( make_dirprod ( make_stn n i li ) ( make_stn m j lj ) ). simpl. apply ( invmaponpathsincl _ ( isinclstntonat _ ) _ _ ). simpl. apply e. - set ( e := natleh0tois0 i ). rewrite e. rewrite ( natmultn0 n ). split with ( @pr2 _ _ ). apply ( isweqtoempty2 _ ( weqstn0toempty ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.